Closing the tail ledger: what the head harvest leaves

R324BracketTailLedger is clause B on the high-frequency region r324CMBracketWeight ε α β ≤ 1. By r324Tail_sum_eq_alphaDecay_mul_headHarvest its left-hand side is exactly

⟨α⟩⁻⁴ · ‖r324TailHeadHarvest ρ ε m α β F i₀‖,

an identity, not an estimate: the two head Green edges G(x - v_{L,0}) and G(z - v_{R,0}) are entity independent, so both external integrations ∫ e^{iαx} … and ∫ e^{-iαz} … are performed with the entity sum still inside the integrand, and each contributes exactly ⟨α⟩⁻² (norm_translatedGreenMode). Because the harvest is an identity, the remaining decay factors still multiply on.

What is left, r324TailHeadHarvest, is the integral over the two innermost variable groups (w, v) of

• the two tail external characters (charT4 β y inside r324TailBetaCoefficient, charT4 (-β) w outside), which must still produce ⟨β⟩⁻⁴, and
• the two transported head characters charT4 α (v_{L,0}), charT4 (-α) (v_{R,0}), which is where the mode α has been moved: it now sits on the internal anchors, against the covariance symbols, and that is the only place the central bracket ⟨‖α+β‖⟩⁻⁸ can come from (momentum conservation).

That statement is isolated as R324BracketTailResidual, and the tail ledger follows from it (R324BracketTailLedger_of_residual).

Unconditionally — with no residual at all — the head harvest already closes the tail ledger on the sub-region where the β endpoint loss is affordable (r324Tail_ledger_of_alpha_suffices).

The unconditional sub-region

theorem Anderson4D.paperFourthOrderModeDecay_le_cmBracketWeight {ε : ℝ} (α β : Z4) (h : 1 ≤ ε⁻¹ ^ 8 * paperFourthOrderModeDecay β * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency (α + β)‖)) : paperFourthOrderModeDecay α ≤ r324CMBracketWeight ε α β

If the β endpoint decay together with the central bracket is paid for by the endpoint loss ε⁻⁸, the α harvest alone already dominates the bracket weight.

theorem Anderson4D.r324Tail_ledger_of_alpha_suffices {ρ : SmoothCutoff} {K : ℝ} (hA : R324CappedDensityLedger ρ K) {ε : ℝ} (m : ℕ) (α β : Z4) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hm2 : 2 ≤ m) (hcap : m ≤ truncOrder ε) (hreg : paperFourthOrderModeDecay α ≤ r324CMBracketWeight ε α β) (F : Finset (MomentContraction m)) : ‖∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ K ^ m * |Real.log ε| ^ (m - 1) * r324CMBracketWeight ε α β

The tail ledger, unconditionally, wherever the α harvest suffices. No residual and no oscillation beyond the two head integrations.

The residual

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

The residual of the tail ledger. Everything the head harvest does not do: the two tail endpoint harvests (⟨β⟩⁻⁴) and the central bracket (⟨‖α+β‖⟩⁻⁸), stated on the object the head harvest leaves behind. Note that this is not a bound on a modulus density — the two transported head characters charT4 α (v_{L,0}), charT4 (-α) (v_{R,0}) sit inside the integral and carry the mode α into the internal covariance sum, which is exactly what the central bracket needs.

Equations

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

theorem Anderson4D.R324BracketTailLedger_of_residual {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324BracketTailResidual ρ K) : R324BracketTailLedger ρ K

The tail ledger from the residual. The head harvest is an identity, so the two decays simply multiply.

theorem Anderson4D.paperFourthOrderModeDecay_pos (k : Z4) : 0 < paperFourthOrderModeDecay k

theorem Anderson4D.R324BracketTailResidual_of_tailPaperLedger {ρ : SmoothCutoff} {K : ℝ} (h : ∀ {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 2 ≤ m → m ≤ truncOrder ε → r324CMBracketWeight ε α β ≤ 1 → ∀ (F : Finset (MomentContraction m)), ‖∑ e ∈ F, deterministicMomentContractionTerm ρ ε m α β e‖ ≤ K ^ m * |Real.log ε| ^ (m - 1) * r324BracketPaperWeight α β) : R324BracketTailResidual ρ K

The residual is not an over-assumption. It is equivalent to the ε-free tail ledger it is used to prove: the head harvest divides out exactly. So R324BracketTailResidual measures precisely the work the head harvest leaves — the two tail endpoint harvests and the central bracket — and nothing more.

theorem Anderson4D.R324CappedBracketDensityLedger_of_residual {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (hA : R324CappedDensityLedger ρ K) (h : R324BracketTailResidual ρ K) : R324CappedBracketDensityLedger ρ K

Clause B from clause A and the residual.

theorem Anderson4D.R324CappedCrossLedgerStrong_of_residual {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (hA : R324CappedDensityLedger ρ K) (h : R324BracketTailResidual ρ K) : R324CappedCrossLedgerStrong ρ K

The strong capped ledger from clause A and the residual.