Clause B at the correct scaling

R324BetaQuadBracketLedger (and with it R324CentralAnchorLedger, R324AnchorCentralBudget) demands the ε-free bracket ⟨‖α+β‖⟩⁻⁸. Clause B itself — R324CappedBracketDensityLedger — asks only for

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

Since ∑_{e∈F} term = ⟨α⟩⁻⁴⟨β⟩⁻⁴ · r324BetaQuadHarvest identically (r324Beta_sum_eq_endpointDecays_mul_quadHarvest), clause B is equivalent to

‖r324BetaQuadHarvest‖ ≤ Kᵐ|log ε|^{m-1} · ε⁻⁸⟨ε‖freq(α+β)‖⟩⁻⁸,

which is R324ScaledQuadBracketLedger below. The ε-free Prop is stronger by at least the factor ε⁻⁸; that over-strengthening is what made the half-symbol route look six orders short.

The chain assembled here is

R324ScaledHalfWindowBudget (window budget) → R324ScaledAnchorCentralBudget (R324ScaledCentralBudget) → R324ScaledCentralAnchorLedger (+ R324AnchorCollapseAt) → R324ScaledQuadBracketLedger (four anchor harvests) → R324CappedBracketDensityLedger (clause B) — with no appeal to clause A and no region hypothesis r324CMBracketWeight ≤ 1.

Nothing is lost: the ε-free ledger implies the scaled one (R324ScaledQuadBracketLedger_of_epsFreeQuad, r324Scaled_epsFree_bracket_le).

The scaled bracket dominates the ε-free one

theorem Anderson4D.r324Scaled_epsFree_bracket_le {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {x : ℝ} (hx : 0 ≤ x) : eighthOrderFrequencyDecay x ≤ ε⁻¹ ^ 8 * eighthOrderFrequencyDecay (ε * x)

The over-strengthening, measured. For 0 < ε ≤ 1 the ε-free bracket is below the scaled bracket with its ε⁻⁸ slack, so every ε-free statement implies its scaled companion — and, by r324Central_epsScale_gap, the converse fails by up to ε⁻¹⁶.

The scaled central-anchor ledger

def Anderson4D.R324ScaledCentralAnchorLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

R324CentralAnchorLedger at the correct scaling. Same object, same estimate, but the bracket is the ε-scaled one that the covariance symbols actually produce. The region hypothesis r324CMBracketWeight ε α β ≤ 1 of the proved Prop is not needed: the scaled bound holds on the whole capped range.

Equations

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

theorem Anderson4D.R324ScaledCentralAnchorLedger_of_collapse_and_budget {ρ : SmoothCutoff} {C D : ℝ} (hC : 0 ≤ C) (hcol : ∀ (m : ℕ), R324AnchorCollapseAt ρ C m) (hbud : R324ScaledAnchorCentralBudget ρ D) : R324ScaledCentralAnchorLedger ρ (C * D)

The scaled central-anchor ledger from the proved collapse and the scaled budget. Exactly R324CentralAnchorLedger_of_collapse_and_budget with the correctly scaled bracket; the collapse input R324AnchorCollapseAt is the proved one, unchanged.

The scaled quadruple-harvest ledger

def Anderson4D.R324ScaledQuadBracketLedger (ρ : SmoothCutoff) (K : ℝ) : Prop

Clause B's exact residue. R324BetaQuadBracketLedger with the bracket clause B really asks for: the ε-scaled bracket together with the ε⁻⁸ endpoint slack. By r324Beta_sum_eq_endpointDecays_mul_quadHarvest this is equivalent to clause B on every entity set (the two endpoint decays divide out exactly).

Equations

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

theorem Anderson4D.R324ScaledQuadBracketLedger_of_scaledCentralAnchor {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324ScaledCentralAnchorLedger ρ K) : R324ScaledQuadBracketLedger ρ (4 * K)

Anchor resolution, at the correct scaling. The proved four-term decomposition r324BetaQuadHarvest_eq_anchorCombination is bracket-agnostic, so the argument of R324BetaQuadBracketLedger_of_centralAnchor transfers verbatim; the ε⁻⁸ slack is picked up at the last step and never used.

Clause B

theorem Anderson4D.R324CappedBracketDensityLedger_of_scaledQuad {ρ : SmoothCutoff} {K : ℝ} (h : R324ScaledQuadBracketLedger ρ K) : R324CappedBracketDensityLedger ρ K

Clause B from the scaled ledger — the whole point. The endpoint identity r324Beta_sum_eq_endpointDecays_mul_quadHarvest turns the scaled quadruple-harvest bound into r324CMBracketWeight exactly: the two endpoint decays multiply back on and the ε⁻⁸ slack is precisely the endpoint loss. No clause A, no region split, no r324CMBracketWeight ≤ 1 hypothesis.

theorem Anderson4D.R324CappedCrossLedgerStrong_of_scaledQuad {ρ : SmoothCutoff} {K : ℝ} (hA : R324CappedDensityLedger ρ K) (h : R324ScaledQuadBracketLedger ρ K) : R324CappedCrossLedgerStrong ρ K

The strong capped ledger: clause A (taken as a hypothesis) plus the scaled ledger.

theorem Anderson4D.R324ScaledQuadBracketLedger_of_epsFreeQuad {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : ∀ {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 2 ≤ m → m ≤ truncOrder ε → ∀ (F : Finset (MomentContraction m)) (hm : 0 < m), ‖r324BetaQuadHarvest ρ ε m α β hm F‖ ≤ K ^ m * |Real.log ε| ^ (m - 1) * eighthOrderFrequencyDecay ‖z4EuclideanFrequency (α + β)‖) : R324ScaledQuadBracketLedger ρ K

Nothing is lost. The ε-free quadruple-harvest ledger — the content of the proved R324BetaQuadBracketLedger, stated without its region hypothesis — implies the scaled one.

theorem Anderson4D.r324Scaled_quad_of_quadBracket {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324BetaQuadBracketLedger ρ K) {ε : ℝ} (m : ℕ) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hcap : m ≤ truncOrder ε) (hW : r324CMBracketWeight ε α β ≤ 1) (F : Finset (MomentContraction m)) (hm : 0 < m) : ‖r324BetaQuadHarvest ρ ε m α β hm F‖ ≤ K ^ m * |Real.log ε| ^ (m - 1) * (ε⁻¹ ^ 8 * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency (α + β)‖))

The proved ε-free ledger implies the scaled bound on its own region of validity.

The theorem, with the anchor bracket Props eliminated

theorem Anderson4D.R324CappedBracketDensityLedger_of_halfWindow {ρ : SmoothCutoff} {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hcol : ∀ (m : ℕ), R324AnchorCollapseAt ρ C m) (hwin : R324ScaledHalfWindowBudget ρ D) : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedBracketDensityLedger ρ K

Clause B, closed, modulo the window budget and the proved collapse. Chaining r324Scaled_anchorCentralBudget_of_halfWindow, R324ScaledCentralAnchorLedger_of_collapse_and_budget, R324ScaledQuadBracketLedger_of_scaledCentralAnchor and R324CappedBracketDensityLedger_of_scaledQuad.

theorem Anderson4D.mainConditional_of_scaledWindowBudget {M : NoiseModel} {ρ : SmoothCutoff} {C D K : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hD : 0 ≤ D) (hA : R324CappedDensityLedger ρ K) (hcol : ∀ (m : ℕ), R324AnchorCollapseAt ρ C m) (hwin : R324ScaledHalfWindowBudget ρ D) : MainConditional M ρ

MainConditional, resting on clause A, the proved anchor collapse, and the window budget alone. R324AnchorCentralBudget — the ε-free central bracket that R324AnchorSuffixCount showed cannot be read off the Green brackets, and that r324Central_epsScale_gap showed the symbols miss by ε⁻¹⁶ — has been eliminated: at the scaling clause B actually needs, the bracket is produced unconditionally by the covariance symbols themselves.

theorem Anderson4D.mainConditional_of_gradedBudget_scaled {M : NoiseModel} {ρ : SmoothCutoff} {C D E K : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hD : 0 ≤ D) (hgrade : ∀ (m : ℕ), R324ColGradedBudgetAt ρ E m r324LayerSplitGrade) (hbridge : (∀ (m : ℕ), R324ColGradedBudgetAt ρ E m r324LayerSplitGrade) → R324CappedDensityLedger ρ K) (hcol : ∀ (m : ℕ), R324AnchorCollapseAt ρ C m) (hwin : R324ScaledHalfWindowBudget ρ D) : MainConditional M ρ

Conditional assembly from the graded lattice budget, anchor collapse, and half-symbol window budget. This restates of mainConditional_of_gradedBudget with the anchor bracket Prop R324AnchorCentralBudget removed: what is left on the clause-B side is a pure window budget with no frequency bracket in it.