General-order peel interface for the R-324 uniform branch

The uniform-branch obligation MomentRefinedIntegratedReductionOutputAt demands, for every residual-refined fibre at order m, the inserted Proposition 4.1 majorant on the right-hand side. This file isolates the one genuinely analytic input of the general-m case as a scalar logarithmic ledger for the refined fibre sums and proves that this ledger exactly funds the majorant:

• |λ_ε|^{2m} = λ^{2m}/|log ε|^m supplies m inverse logarithms;
• a fibre obeying ‖·‖ ≤ K^m |log ε|^{m-1} therefore lands at K^m λ^{2m}/|log ε|;
• the integrated inserted majorant is at least (C₀ λ)^{2m}/|log ε| at support constant 1 (le_integral_primitiveInsertedMajorant), so the geometric absorption K^m ≤ (K+1)^{2m} closes the estimate with the m-independent primitive constant C₀ = K + 1.

No triangle inequality across fibres and no factorial count appears: the ledger is stated for the summed fibre, matching the cancellation-preserving interface of R324PrimitiveIterationClosure.

The general-order fibre ledger

def Anderson4D.R324GeneralPeelFibreLogBound (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (K : ℝ) : Prop

The per-fibre logarithmic ledger at order m. Each residual-refined fibre sum, taken before any norm is moved inside, is bounded by K^m |log ε|^{m-1}: one geometric factor per order and one logarithm per block beyond the first, exactly the paper Section 4.2 Step 2--3 output.

Equations

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

theorem Anderson4D.r324GeneralPeel_abs_lamEps_pow (lam : ℝ) {ε : ℝ} (hlog : 1 ≤ |Real.log ε|) (m : ℕ) : |lamEps lam ε| ^ (2 * m) = lam ^ (2 * m) / |Real.log ε| ^ m

The coupling weight splits into m inverse logarithms.

The ledger funds the inserted majorant

theorem Anderson4D.momentRefinedIntegratedReductionOutputAt_of_generalPeelFibreLogBound {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {K : ℝ} (hm : 1 ≤ m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hK : 0 ≤ K) (h : R324GeneralPeelFibreLogBound ρ ε m α β K) : MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β (K + 1) 1

The general-order uniform-branch bridge. At every order m ≥ 1, the per-fibre logarithmic ledger discharges the integrated residual-refined reduction obligation with the m-independent primitive constant K + 1 and support constant 1. The m inverse logarithms of |λ_ε|^{2m} pay for the m - 1 fibre logarithms, and the last inverse logarithm is matched by the near-field mass of the inserted majorant.

The uniform general-order ledger

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

The remaining general-order input, as one clean proposition. A single mollifier-dependent geometric constant funds the per-fibre logarithmic ledger at every order and both external modes. By momentRefinedIntegratedReductionOutputAt_of_generalPeelFibreLogBound this is precisely what separates the closed low orders from the full uniform branch.

Equations

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

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

Strongest per-cutoff output form. One primitive constant, chosen from the mollifier alone, discharges the uniform-branch obligation at every order m ≥ 1, every coupling, every admissible scale, and both external modes, at support constant 1.