Unconditional routed outputs from the low-order window ledgers

Composition layer over R324RoutedEvalLowOrder:

• both routed window Props are monotone in the window constant, so the two order-one ledgers can be served by one constant;
• exists_r324RoutedWindowLedger_one — one cutoff-only constant funds both routed Props at m = 1;
• exists_countableCentralRoutedMomentReductionOutput_one — the countable central routed output of the proved reduction chain holds unconditionally at m = 1, at the windowed amplitude λ_ε²·(16·C·λ⁰) times the endpoint loss.

R324RoutedWindowLedgerAt states the general-order estimate. The α+β ≠ 0 ledger for m ≥ 2 and the zero-shift ledger for m ≥ 3 are not provable by the norm-inside route weights (the free cross slots of a two-cross contraction pay the full coefficient mass ε⁻⁴ instead of one retained Green window C·L), so they require the finer physical evaluation used by the final proof.

theorem Anderson4D.R324RoutedPerTermWindowBound.mono {ρ : SmoothCutoff} {lam : ℝ} {m : ℕ} {C C' : ℝ} (h0 : 0 ≤ C) (hCC : C ≤ C') (h : R324RoutedPerTermWindowBound ρ lam m C) : R324RoutedPerTermWindowBound ρ lam m C'

The nonzero-shift routed ledger is monotone in the window constant.

theorem Anderson4D.R324RoutedZeroShiftWindowBound.mono {ρ : SmoothCutoff} {lam : ℝ} {m : ℕ} {C C' : ℝ} (h0 : 0 ≤ C) (hCC : C ≤ C') (h : R324RoutedZeroShiftWindowBound ρ lam m C) : R324RoutedZeroShiftWindowBound ρ lam m C'

The zero-shift routed ledger is monotone in the window constant.

def Anderson4D.R324RoutedWindowLedgerAt (ρ : SmoothCutoff) (lam C : ℝ) (m : ℕ) : Prop

The complete routed window ledger at one order. This is the exact pair of Props consumed by the proved frozen-amplitude routed reduction; it is fully proved here at m = 1, while for m ≥ 2 the nonzero-shift half remains the open physical obligation.

Equations

• Anderson4D.R324RoutedWindowLedgerAt ρ lam C m = (Anderson4D.R324RoutedPerTermWindowBound ρ lam m C ∧ Anderson4D.R324RoutedZeroShiftWindowBound ρ lam m C)

theorem Anderson4D.exists_r324RoutedWindowLedger_one (ρ : SmoothCutoff) (lam : ℝ) : ∃ (C : ℝ), 0 < C ∧ R324RoutedWindowLedgerAt ρ lam C 1

Both routed window Props hold at order one, with a single constant depending only on the cutoff.

theorem Anderson4D.exists_countableCentralRoutedMomentReductionOutput_one (ρ : SmoothCutoff) (lam : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ truncOrder ε → ∀ (α β : Z4), CountableCentralRoutedMomentReductionOutput ρ lam ε 1 α β (lamEps lam ε ^ 2 * (16 * C ^ 1 * lam ^ (2 * 1 - 2)) * r324EndpointLoss ε α β)

The unconditional order-one routed output. The countable central routed moment reduction output holds at m = 1 at the windowed amplitude, with a constant depending only on the cutoff.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_refinedIntegrated_and_ledger {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε C : ℝ) (m : ℕ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → m ≤ truncOrder ε → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → R324RoutedWindowLedgerAt ρ lam C m → 16 * C ^ m * lam ^ (2 * m - 2) ≤ outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

The conditional endgame, restated on the named ledger. The deterministic paper bound needs, beyond the proved uniform-branch output, exactly one R324RoutedWindowLedgerAt instance per order together with the ε-free amplitude comparison; order one of that ledger is unconditional by exists_r324RoutedWindowLedger_one.