The conditional main theorem

This file supplies the closed paper-order estimates from Section 4.2 and assembles the conditional theorem. The Gabriel--Rosati input remains an explicit premise inside MainConditional; no unconditional theorem is declared.

theorem Anderson4D.deterministic_second_moment_bound (rho : SmoothCutoff) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (epsilon : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder epsilon → ∀ (alpha beta : Z4), ‖deterministicMomentPairingSum rho lam epsilon m alpha beta‖ ≤ paperDeterministicMomentRHS outerC powerC lam epsilon m alpha beta

P-3.5b-det / paper (3.24), closed. The deterministic pairing sum obeys the paper's second-moment bound, including all three Fourier decay factors, with constants depending only on the cutoff.

theorem Anderson4D.main_conditional (M : NoiseModel) (rho : SmoothCutoff) : MainConditional M rho

Conditional Deng--Shen Theorem 1.1. For every noise model and cutoff, the uniform Gabriel--Rosati input implies the finite-family Fourier-mode characteristic-function statement MainStatement.

theorem Anderson4D.main_conditional_law (M : NoiseModel) (rho : SmoothCutoff) : Prop36Family M rho → MainLawStatement M rho

Conditional Deng--Shen Theorem 1.1 in the advertised finite-family convergence-in-distribution form. Proposition 3.6 remains the sole explicit external hypothesis.