Closing paper Steps 2--3 on every residual-refined fibre

This capstone combines the exact signed two-half collapse with the complete nested-run endpoint estimate. The only case split is the literal one on a refined representative: zero coupling, full/full, or a nonempty residual carrier. No modulus is taken before all within-half and cross-block collapses have finished.

The nonempty initial nested-cross suffix

theorem Anderson4D.exists_r324InitialNestedCross_head_of_singles_nonempty {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hsingles : κp.singles.Nonempty) : ∃ (head : R324NestedCrossBlock κp κm π) (tail : List (R324NestedCrossBlock κp κm π)), (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail

A surviving single forces the canonical nested cross schedule to have a first block.

theorem Anderson4D.momentContraction_singles_nonempty_or_both_isFull {m : ℕ} (e : MomentContraction m) : e.fst.singles.Nonempty ∨ e.fst.IsFull ∧ e.snd.fst.IsFull

The literal within-half pairings of any moment contraction are either both full or carry a left residual single.

Exact signed endpoint collapse

theorem Anderson4D.lamEps_pow_momentRefinedDeterministicTermSum_eq_initialNestedEndpoint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace leftScale) (rightTrace : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace rightScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (hs : s ∈ momentContractionSignatures m) (hr : r ∈ momentResidualChainSignaturesAt m s) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (hκp : e₀.fst = κp) (hκm : e₀.snd.fst = κm) (hπ : e₀.snd.snd ≍ π) (hε : 0 < ε) (hε1 : ε ≤ 1) : let terminal := R324TwoHalfTerminalData.ofCertifiedTraces leftTrace rightTrace; ↑(lamEps lam ε) ^ (2 * ((R324WithinHalfResidualPrefix.initial ρ lam ε κp).remainingOrder + (R324WithinHalfResidualPrefix.initial ρ lam ε κm).remainingOrder)) * momentRefinedDeterministicTermSum ρ ε m α β s r = ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure

One residual-refined deterministic fibre, multiplied only by the two within-half coupling powers, is exactly the signed endpoint-integrated nested residual density.

Uniform closure of paper Steps 2--3

theorem Anderson4D.exists_r324PaperRefinedStep23Input (ρ : SmoothCutoff) : ∃ (primitiveConstant : ℝ) (supportConstant : ℝ), 0 < primitiveConstant ∧ 0 < supportConstant ∧ R324PaperRefinedStep23Input ρ primitiveConstant supportConstant

One pair of cutoff-dependent constants closes paper Steps 2--3 on every residual-refined fibre. Both constants are selected before the coupling, mollification scale, perturbative order, and external Fourier modes.