The Green-windowed routed budget at the frozen paper amplitude

(A) The exact routed obligation. The capstone consumer exists_deterministicMoment_paper_bound_of_refinedIntegrated_and_countable fixes outerConstant from (primitiveConstant, supportConstant) alone and then demands, at every admissible (ρ, lam, ε, m, α, β), the routed output at the frozen amplitude

CountableCentralRoutedMomentReductionOutput ρ lam ε m α β ((lamEps lam ε ^ 2 * outerConstant * ((16 * primitiveConstant) * lam) ^ (2*m-2)) * r324EndpointLoss ε α β),

with r324EndpointLoss ε α β = ε⁻⁸ · ⟨α⟩⁻⁴ · ⟨β⟩⁻⁴. Through the two proved honest constructors this is equivalent to two scalar ledgers on the exact route weights (both already carrying the endpoint factor 16⟨α⟩⁻⁴⟨β⟩⁻⁴ extracted from the four endpoint Fourier integrations):

• α + β ≠ 0: ∑'_{(p,route)} r324RefinedEndpointNonzeroRouteWeight ≤ W;
• α + β = 0: ∑'_{(p,n)} r324ZeroShiftGroupedWeight ≤ W.

Since |λ_ε|^{2m} · L^{m-1} = λ_ε² · λ^{2m-2} / 1 (with L = |log ε|), the frozen amplitude is reached iff the physical route mass obeys the Green-windowed value — one endpoint sacrifice ε⁻⁸ for the marked pair and one diagonal Green window C·L for each of the other m - 1 pairs:

∑' weights ≤ 16⟨α⟩⁻⁴⟨β⟩⁻⁴ · |λ_ε|^{2m} · C^m · L^{m-1} · ε⁻⁸,

together with the ε-free comparison 16 · C^m · λ^{2m-2} ≤ outerConstant · ((16·primitiveConstant)·λ)^{2m-2}. This file states the windowed ledgers as the two named Props below, proves the general-m reduction (routed output at the frozen amplitude from the Props), and composes with the capstone consumer.

The scalar raw ledger cannot discharge these Props' role: its raw mass already scales as c·ε⁻¹² at m = 1, against a target of K·ε⁻⁸. The Props instead live on the route weights themselves — physical integrals of the fibre-summed internal core with the Green skeleton still inside — not on the norm-inside raw covariance series, so the raw total-mass obstruction does not apply to them.

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

The routed per-term window ledger (nonzero shift). The total corrected nonzero-route weight — per term the physical integral of the signed fibre-summed internal core with its routing slot costs, the Green windows retained — is bounded by the windowed value C^m · L^{m-1} · ε⁻⁸ at the coupling weight |λ_ε|^{2m} and the extracted endpoint factor. This is the routed-branch analogue of the uniform branch's R324GeneralPeelFibreLogBound: same physical layer (norm after the fibre sum), with the route resolution and one marked slot cost added, and the value upgraded from K^m·L^{m-1} to C^m·L^{m-1}·ε⁻⁸ by the endpoint sacrifice.

Equations

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

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

The zero-shift window ledger. The same windowed value bounds the grouped zero-shift weights (the α + β = 0 branch, where every routed increment is zero and no central decay is spent).

Equations

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

theorem Anderson4D.r324RoutedWindow_budget_eq {lam ε C : ℝ} (hlog : 1 ≤ |Real.log ε|) {m : ℕ} (hm : 0 < m) (α β : Z4) : 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * (|lamEps lam ε| ^ (2 * m) * (C ^ m * |Real.log ε| ^ (m - 1) * ε⁻¹ ^ 8)) = lamEps lam ε ^ 2 * (16 * C ^ m * lam ^ (2 * m - 2)) * r324EndpointLoss ε α β

Amplitude bookkeeping. The windowed physical value is the endpoint-loss form of the amplitude λ_ε² · (16·C^m·λ^{2m-2}): |λ_ε|^{2m} · L^{m-1} collapses to λ_ε² · λ^{2m-2} exactly.

theorem Anderson4D.countableCentralRoutedMomentReductionOutput_of_routedWindow {ρ : SmoothCutoff} {lam ε C : ℝ} {m : ℕ} (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (hnonzero : R324RoutedPerTermWindowBound ρ lam m C) (hzero : R324RoutedZeroShiftWindowBound ρ lam m C) (α β : Z4) : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * (16 * C ^ m * lam ^ (2 * m - 2)) * r324EndpointLoss ε α β)

The general-m routed reduction. The two windowed ledgers produce the countable central routed output at the amplitude λ_ε² · (16·C^m·λ^{2m-2}) times the endpoint loss, for every external mode pair — the exact interface consumed by the pigeonhole file and the capstone closure.

theorem Anderson4D.countableCentralRoutedMomentReductionOutput_frozen_of_routedWindow {ρ : SmoothCutoff} {lam ε C outerConstant primitiveConstant : ℝ} {m : ℕ} (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) (hnonzero : R324RoutedPerTermWindowBound ρ lam m C) (hzero : R324RoutedZeroShiftWindowBound ρ lam m C) (hclose : 16 * C ^ m * lam ^ (2 * m - 2) ≤ outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2)) (α β : Z4) : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2) * r324EndpointLoss ε α β)

Landing at the paper amplitude. With the ε-free constant comparison 16·C^m·λ^{2m-2} ≤ outer·((16·C₀)·λ)^{2m-2}, the windowed ledgers deliver the routed output at the exact paper amplitude.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_refinedIntegrated_and_routedWindow {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 → R324RoutedPerTermWindowBound ρ lam m C → R324RoutedZeroShiftWindowBound ρ lam m C → 16 * C ^ m * lam ^ (2 * m - 2) ≤ outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

(E) The conditional endgame. The two windowed route ledgers are, together with the uniform-branch reduction output, sufficient for the complete deterministic paper bound: the routed half of hdet at the paper amplitude follows from countableCentralRoutedMomentReductionOutput_frozen_of_routedWindow inside the final consumer. The outer constant is chosen before the cutoff, coupling, scale, order, Fourier modes, and window constant.