Clause B: the bulk region is already clause A #

R324CappedBracketDensityLedger (clause B) grades its right-hand side by r324CMBracketWeight ε α β = ε⁻⁸ ⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε‖α+β‖⟩⁻⁸. This weight is not small everywhere: the endpoint loss ε⁻⁸ is large, and for every (α, β) in the bulk region

(1 + |α|²)(1 + |β|²) ≤ ε⁻⁴/4 and ε‖freq(α+β)‖ ≤ 1

the weight is at least 1 (one_le_r324CMBracketWeight_of_bulk). On that region clause B is a strictly weaker statement than clause A, and is proved here outright from it (r324Bracket_norm_sum_le_of_one_le_weight): the modulus route is legitimate exactly where the weight has no decay to supply.

What survives is the tail region r324CMBracketWeight ε α β ≤ 1, where the mode grading is real and, by r324CMFlatDensity_modes_indep, must come from the oscillation of the four external characters. That residue is isolated as R324BracketTailLedger, and clause B is proved from clause A plus it (R324CappedBracketDensityLedger_of_tail).

Note the tail region is genuinely a high-frequency region: it forces (1+|α|²)²(1+|β|²)²(1+ε²‖α+β‖²)⁴ ≥ ε⁻⁸, i.e. either an external mode of size ≳ ε⁻¹ or a conserved mode α+β of size ≫ ε⁻¹. This is the same split the paper makes in §4.2.

The modulus route, valid exactly where the weight is `≥ 1` #

source

theorem Anderson4D.r324Bracket_norm_sum_le_of_one_le_weight {ρ : SmoothCutoff} {K : ℝ} (hA : R324CappedDensityLedger ρ K) {ε : ℝ} (m : ℕ) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hcap : m ≤ truncOrder ε) (hW : 1 ≤ r324CMBracketWeight ε α β) (F : Finset (MomentContraction m)) :

‖∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ K ^ m * |Real.log ε| ^ (m - 1) * r324CMBracketWeight ε α β

Clause A gives clause B wherever the weight has no decay to supply. The Bochner triangle inequality plus mode independence of the flat density; no oscillation is used, and none is needed because the weight is ≥ 1.

The bulk region #

source

theorem Anderson4D.one_le_r324CMBracketWeight_of_bulk {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hcentral : ε * ‖z4EuclideanFrequency (α + β)‖ ≤ 1) (hmodes : (1 + paperModeNormSq α) * (1 + paperModeNormSq β) ≤ ε⁻¹ ^ 4 / 4) :

1 ≤ r324CMBracketWeight ε α β

The bulk region carries no decay. If the conserved mode α+β is below the cutoff scale and the two external modes are not too large, the endpoint loss ε⁻⁸ dominates every decay factor and the bracket weight is at least one.

The tail residue and clause B #

source

def Anderson4D.R324BracketTailLedger (ρ : SmoothCutoff) (K : ℝ) :

Prop

The tail ledger. Clause B restricted to the region where the bracket weight really does carry decay. This is the only part of clause B that needs the oscillation of the four external characters: by r324CMFlatDensity_modes_indep no modulus bound can reach it.

Equations