Closure of the uniform branch over the two residual case ledgers

The composition theorem of the interface file and the pure-cross reduction of the cross file leave exactly two analytic obligations:

• R324LedgerThreeCrossLedger, reduced here further to a phase-free integral bound for the nonnegative pure-cross density (r324LedgerThreeCrossLedger_of_integral_bound) — the two-chain multi-window estimate;
• R324LedgerThreeMixedLedger — the fibres retaining a within-half pair, to be peeled by the parity/difference gain.

Given both, the complete uniform branch follows: one per-cutoff primitive constant discharges MomentRefinedIntegratedReductionOutputAt at every order m ≥ 1, every coupling, every admissible scale and both external modes, at support constant one.

The cross ledger from the phase-free integral bound

theorem Anderson4D.r324LedgerThree_integrable_crossDensity (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (hfib : R324LedgerThreeCrossFibre m s r) : MeasureTheory.Integrable (r324LedgerThreeCrossDensity ρ ε m (momentRefinedContractionFiber m s r)) (r324PhysicalMeasure m)

The summed pure-cross density is integrable: it is almost everywhere the norm of the integrable summed flat fibre.

theorem Anderson4D.r324LedgerThreeCrossLedger_of_integral_bound (ρ : SmoothCutoff) (K : ℝ) (h : ∀ {ε : ℝ} (m : ℕ), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 3 ≤ m → ∀ (F : Finset (MomentContraction m)), (∀ e ∈ F, R324LedgerThreeAllCrossEntity e) → ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m F p ∂r324PhysicalMeasure m ≤ K ^ m * |Real.log ε| ^ (m - 1)) : R324LedgerThreeCrossLedger ρ K

The cross-case ledger follows from a phase-free integral bound: it suffices to bound the physical integral of the nonnegative pure-cross density — two plain Green chains against the permutation covariance sum — with no reference to the external modes.

The multi-window integrand

noncomputable def Anderson4D.r324LedgerThreeWindowIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (p : R324PhysicalPoint m) : ℝ

The phase-free two-chain multi-window integrand: two plain Green chains against the product of the m covariance row sums. This is the fibre-independent quantity that funds the entire cross case.

Equations

• Anderson4D.r324LedgerThreeWindowIntegrand ρ ε m p = Anderson4D.r324LedgerThreeLeftChain m p * Anderson4D.r324LedgerThreeRightChain m p * Anderson4D.r324LedgerThreeCrossMajorant ρ ε m p.2.2.2.2

theorem Anderson4D.r324LedgerThree_measurable_crossMajorant (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) : Measurable fun (p : R324PhysicalPoint m) => r324LedgerThreeCrossMajorant ρ ε m p.2.2.2.2

The row-sum majorant is jointly measurable on the physical space.

theorem Anderson4D.exists_r324LedgerThreeCrossMajorant_bound (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) : ∃ (B : ℝ), ∀ (v : Fin (2 * m) → T4), r324LedgerThreeCrossMajorant ρ ε m v ≤ B

The row-sum majorant is uniformly bounded at each fixed scale by the O(ε⁻⁴) covariance height.

theorem Anderson4D.r324LedgerThree_integrable_chainProduct (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) : MeasureTheory.Integrable (fun (p : R324PhysicalPoint m) => r324LedgerThreeLeftChain m p * r324LedgerThreeRightChain m p) (r324PhysicalMeasure m)

The bare two-chain product is integrable: the proved doubled profile integrability at the identity pairings.

theorem Anderson4D.r324LedgerThree_integrable_windowIntegrand (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) : MeasureTheory.Integrable (r324LedgerThreeWindowIntegrand ρ ε m) (r324PhysicalMeasure m)

The multi-window integrand is integrable at every fixed admissible scale: the chains carry the integrable mass and the row-sum majorant is a bounded measurable factor.

theorem Anderson4D.r324LedgerThree_integral_crossDensity_le_windowIntegral (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {F : Finset (MomentContraction m)} (hF : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) : ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m F p ∂r324PhysicalMeasure m ≤ ∫ (p : R324PhysicalPoint m), r324LedgerThreeWindowIntegrand ρ ε m p ∂r324PhysicalMeasure m

The pure-cross fibre integral is dominated by the multi-window integral: the pointwise permanent bound integrates against the integrable majorant.

theorem Anderson4D.r324LedgerThreeCrossLedger_of_windowIntegral_bound (ρ : SmoothCutoff) (K : ℝ) (h : ∀ {ε : ℝ} (m : ℕ), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 3 ≤ m → ∫ (p : R324PhysicalPoint m), r324LedgerThreeWindowIntegrand ρ ε m p ∂r324PhysicalMeasure m ≤ K ^ m * |Real.log ε| ^ (m - 1)) : R324LedgerThreeCrossLedger ρ K

Cross-case ledger from the multi-window integral bound: the sharpest residual form of the cross case. The obligation no longer mentions fibres, signatures, or external modes — it is one scalar integral inequality for the two plain chains against the m covariance row sums.

The final uniform-branch statement

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

The complete uniform branch over the residual case ledgers. Given the two residual case ledgers — the pure-cross multi-window bound and the mixed parity-gain bound, each with a per-cutoff constant — every order m ≥ 1 of the uniform branch closes at one primitive constant and support constant one.

theorem Anderson4D.exists_momentRefinedIntegratedReductionOutputAt_of_window_and_mixed (ρ : SmoothCutoff) (hwin : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {ε : ℝ} (m : ℕ), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 3 ≤ m → ∫ (p : R324PhysicalPoint m), r324LedgerThreeWindowIntegrand ρ ε m p ∂r324PhysicalMeasure m ≤ K ^ m * |Real.log ε| ^ (m - 1)) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324LedgerThreeMixedLedger ρ K) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (lam : ℝ) {ε : ℝ} (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → MomentRefinedIntegratedReductionOutputAt ρ lam ε m α β C₀ 1

Sharpest conditional form. The complete uniform branch from the two terminal residual obligations: the fibre-free multi-window integral bound and the mixed-fibre ledger.