The correctly scaled central bracket, and where it comes from

R324AnchorCentralBudget asks the anchor lattice series to carry the ε-free bracket ⟨‖α+β‖⟩⁻⁸. That is stronger than clause B needs: clause B's own weight is

r324CMBracketWeight ε α β = ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴ · ⟨ε‖freq(α+β)‖⟩⁻⁸,

whose bracket is ε-scaled and which carries a spare ε⁻⁸. The ε-free demand exceeds the honest target by at least ε⁻⁸, and that excess is exactly the shortfall which made the half-symbol route look impossible (r324Central_epsScale_gap).

At the correct scaling the half-symbol route works, unconditionally:

• one power of the covariance symbol already carries a full eighth-order bracket at the ε-scaled key (r324Scaled_exists_symbolBracket, the order-8 Schwartz bound of SmoothCutoff);
• the momentum sector forces ∑ᵢ qᵢ = -(α+β), so the product bracket r324HdetAssembly_prod_eighthDecay_le at aᵢ = ε‖freq qᵢ‖ collapses the m per-key brackets into m⁴ · ⟨ε‖freq(α+β)‖⟩⁻⁸ (r324Scaled_halfSym_le_bracket);
• the remaining half of each symbol, ∏ᵢ‖ρ̂(εqᵢ)‖, is left to fund the window sums, and that is stated as the named hypothesis R324ScaledHalfWindowBudget — the proved window-budget shape (R324ColGradedBudgetAt at the flat grade m-1, R324AnchorCentralBudget minus its bracket) with the symbol at half power and no bracket demanded on the right.

The output is R324ScaledAnchorCentralBudget, the honest replacement of R324AnchorCentralBudget, with the ε⁻⁸ slack still unspent.

One power of the symbol carries the eighth-order bracket

theorem Anderson4D.r324Scaled_exists_symbolBracket (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε : ℝ}, 0 < ε → ∀ (k : Z4), ‖ρ.symbol ε k‖ ≤ C * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency k‖)

The single-power symbol bracket. The order-8 Schwartz decay of ρ̂ gives ‖ρ̂(εk)‖ ≤ C⟨ε‖k‖⟩⁻⁸ — a whole eighth-order bracket per key from one of the two symbol factors, the 2π Fourier normalization absorbed into C. This is the half-symbol split of r324HdetAssembly_exists_halfSymbol_sq_bracket in the form the product bracket consumes.

The half-symbol weight

noncomputable def Anderson4D.r324ScaledHalfSym (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (q : Fin m → Z4) : ℝ

The remaining half of the symbol weight: one power of ρ̂(εqᵢ) per key instead of two. r324ColLatSym is its square.

Equations

• Anderson4D.r324ScaledHalfSym ρ ε q = ∏ i : Fin m, ‖ρ.symbol ε (q i)‖

theorem Anderson4D.r324ScaledHalfSym_nonneg (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (q : Fin m → Z4) : 0 ≤ r324ScaledHalfSym ρ ε q

theorem Anderson4D.r324ColLatSym_eq_halfSym_mul (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (q : Fin m → Z4) : r324ColLatSym ρ ε q = r324ScaledHalfSym ρ ε q * r324ScaledHalfSym ρ ε q

The product bracket on the conservation sector

theorem Anderson4D.r324Scaled_halfSym_le_bracket (ρ : SmoothCutoff) {C : ℝ} (hC : 0 ≤ C) (hsym : ∀ {ε : ℝ}, 0 < ε → ∀ (k : Z4), ‖ρ.symbol ε k‖ ≤ C * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency k‖)) {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : 1 ≤ m) (γ : Z4) (q : Fin m → Z4) (hq : ∑ i : Fin m, q i = γ) : r324ScaledHalfSym ρ ε q ≤ C ^ m * ↑m ^ 4 * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency γ‖)

The central bracket, harvested. On the momentum sector ∑ᵢ qᵢ = γ the half-symbol weight is bounded by Cᵐ·m⁴ times the eighth-order bracket at the conserved mode, at the ε-scaled frequency. No zone split, no endpoint trade: the product bracket r324HdetAssembly_prod_eighthDecay_le and momentum conservation do all the work.

theorem Anderson4D.r324Scaled_norm_freq_neg (k : Z4) : ‖z4EuclideanFrequency (-k)‖ = ‖z4EuclideanFrequency k‖

The half-symbol anchor weight and the window budget

noncomputable def Anderson4D.r324ScaledHalfAnchorWeight (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (aL aR : ℕ) (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : ℝ

The anchor lattice summand with the symbol at half power: what is left after the product bracket has been harvested.

Equations

• Anderson4D.r324ScaledHalfAnchorWeight ρ ε α β aL aR τ q = Anderson4D.r324ScaledHalfSym ρ ε q * (Anderson4D.r324AnchorLatProp α β aL q * Anderson4D.r324AnchorLatProp α β aR (q ∘ ⇑τ))

theorem Anderson4D.r324ScaledHalfAnchorWeight_nonneg (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (aL aR : ℕ) (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : 0 ≤ r324ScaledHalfAnchorWeight ρ ε α β aL aR τ q

def Anderson4D.R324ScaledHalfWindowBudget (ρ : SmoothCutoff) (D : ℝ) : Prop

The window budget, at half symbol power. Exactly the proved window-budget shape — R324ColGradedBudgetAt ρ D m at the flat grade m-1, equivalently R324AnchorCentralBudget — with two changes: the lattice symbol weight sits at half power (the other half has been spent on the central bracket) and no frequency bracket is demanded on the right.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.r324Scaled_anchorLatWeight_le_half (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) (aL aR : ℕ) (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : r324AnchorLatWeight ρ ε α β aL aR τ q ≤ r324ScaledHalfAnchorWeight ρ ε α β aL aR τ q

How the half-symbol budget relates to the proved one. Since ‖ρ̂(εk)‖ ≤ 1, the half-symbol weight dominates the proved anchor lattice weight pointwise. So R324ScaledHalfWindowBudget is exactly the proved window budget with the symbol at half power — the same statement about the same Schwartz-decaying symbol, and the only price paid for the central bracket.

def Anderson4D.R324ScaledAnchorCentralBudget (ρ : SmoothCutoff) (D : ℝ) : Prop

The correctly scaled central lattice budget. The honest replacement of R324AnchorCentralBudget: the bracket at the conserved mode is the ε-scaled one, which is all r324CMBracketWeight demands, and the ε⁻⁸ endpoint slack is not spent here at all.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.r324Scaled_anchorLatWeight_le (ρ : SmoothCutoff) {C : ℝ} (hC : 0 ≤ C) (hsym : ∀ {ε : ℝ}, 0 < ε → ∀ (k : Z4), ‖ρ.symbol ε k‖ ≤ C * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency k‖)) {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : 1 ≤ m) (α β : Z4) (bL bR : ℕ) (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) (hq : ∑ i : Fin m, q i = -(α + β)) : r324AnchorLatWeight ρ ε α β bL bR τ q ≤ C ^ m * ↑m ^ 4 * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency (α + β)‖) * r324ScaledHalfAnchorWeight ρ ε α β bL bR τ q

The pointwise harvest. On the conservation sector every anchor lattice summand is the scaled central bracket times its half-symbol companion.

theorem Anderson4D.r324Scaled_cast_pow_four_le (m : ℕ) : ↑m ^ 4 ≤ 16 ^ m

The scaled central budget, proved

theorem Anderson4D.r324Scaled_anchorCentralBudget_of_halfWindow {ρ : SmoothCutoff} {D : ℝ} (hD : 0 ≤ D) (hbud : R324ScaledHalfWindowBudget ρ D) : ∃ (E : ℝ), 0 ≤ E ∧ R324ScaledAnchorCentralBudget ρ E

The correctly scaled central budget, from the window budget alone. This is the step that r324Central_epsScale_gap shows is impossible for the ε-free target and which is unconditional here: the covariance symbols only ever see εk, and the ε-scaled bracket is exactly what they produce. The ε⁻⁸ slack of r324CMBracketWeight is never touched.