Closure of the general peel ledger at the proved orders

This file instantiates the general peel interface:

• order one satisfies the fibre ledger unconditionally (no logarithm is spent), so MomentRefinedIntegratedReductionOutputAt holds at m = 1 with a universal primitive constant;
• together with the proved unconditional order-two closure, both low orders hold at one common per-cutoff constant;
• consequently the only remaining uniform-branch obligation is the fibre ledger R324GeneralPeelFibreLogBound at orders m ≥ 3, and the final theorem turns any such ledger into the full uniform-branch output at every order m ≥ 1 with one constant.

The order-one ledger

theorem Anderson4D.r324GeneralPeel_fibreLogBound_one (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : R324GeneralPeelFibreLogBound ρ ε 1 α β ((2 * Real.pi) ^ dim)

The order-one fibre ledger holds unconditionally. A refined fibre contains at most the unique order-one contraction, whose term is bounded by the paper volume; K^1 |log ε|^0 demands no logarithm.

theorem Anderson4D.exists_momentRefinedIntegratedReductionOutputAt_one (ρ : SmoothCutoff) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → MomentRefinedIntegratedReductionOutputAt ρ lam ε 1 α β C₀ 1

The unconditional order-one uniform-branch output.

The order-two ledger

theorem Anderson4D.R324GeneralPeelFibreLogBound.mono {ρ : SmoothCutoff} {ε : ℝ} {m : ℕ} {α β : Z4} {K K' : ℝ} (hK : 0 ≤ K) (hKK' : K ≤ K') (hlog : 1 ≤ |Real.log ε|) (h : R324GeneralPeelFibreLogBound ρ ε m α β K) : R324GeneralPeelFibreLogBound ρ ε m α β K'

The fibre ledger is monotone in its geometric constant.

theorem Anderson4D.exists_r324GeneralPeel_fibreLogBound_two (ρ : SmoothCutoff) : ∃ (K : ℝ), 0 < K ∧ ∀ {ε : ℝ} (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R324GeneralPeelFibreLogBound ρ ε 2 α β K

The order-two fibre ledger holds unconditionally: the two-block fibre is the product of two uniformly bounded halves (spending no logarithm), and every cross fibre spends its diagonal window logarithm, matching K^2 |log ε|^1 exactly. This verifies that the general peel normalization is the correct induction invariant at both closed orders.

theorem Anderson4D.exists_r324GeneralPeel_fibreLogBound_le_two (ρ : SmoothCutoff) : ∃ (K : ℝ), 0 < K ∧ ∀ {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → m ≤ 2 → R324GeneralPeelFibreLogBound ρ ε m α β K

Both closed orders satisfy the ledger at one per-cutoff constant.

Combining orders at one constant

theorem Anderson4D.MomentRefinedIntegratedReductionOutputAt.mono_primitiveConstant {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {C C' : ℝ} (hC : 0 ≤ C) (hCC' : C ≤ C') (hε : 0 < ε) (h : MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β C 1) : MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β C' 1

The uniform-branch output is monotone in the primitive constant.

theorem Anderson4D.exists_momentRefinedIntegratedReductionOutputAt_le_two (ρ : SmoothCutoff) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → m ≤ 2 → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β C₀ 1

Both low orders at one per-cutoff constant. Order one is the new unconditional output; order two is the proved unconditional closure.

The exact residual obligation

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

The single remaining uniform-branch obligation. One per-cutoff geometric constant funds the fibre logarithmic ledger at every order m ≥ 3. Orders one and two are closed unconditionally above; by the general peel bridge this proposition is all that separates the project from the complete middle estimate.

Equations

• Anderson4D.R324GeneralPeelLedgerFromThree ρ K = ∀ {ε : ℝ} (m : ℕ) (α β : Anderson4D.Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 3 ≤ m → Anderson4D.R324GeneralPeelFibreLogBound ρ ε m α β K

theorem Anderson4D.exists_momentRefinedIntegratedReductionOutputAt_of_ledgerFromThree (ρ : SmoothCutoff) (h : ∃ (K : ℝ), 0 ≤ K ∧ R324GeneralPeelLedgerFromThree ρ K) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β C₀ 1

Master closure of the uniform branch. Any ledger for the orders m ≥ 3 yields the complete uniform-branch output: one per-cutoff primitive constant, every order m ≥ 1, every coupling, every admissible scale, both external modes, support constant one.