Direct deterministic closure of the conditional main theorem

This file uses the paper's quantifier order: the uniform and routed branches produce one fixed absolute constant, which may subsequently be enlarged. A single deterministic (3.24) bound produces MainSecondMomentInput through the concrete Fubini and Wick laws, and the same bound is then reused by the measurable good-event construction.

theorem Anderson4D.mainSecondMomentInput_of_deterministicMomentBound {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant : ℝ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hdet : ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) : MainSecondMomentInput M ρ (√outerConstant) powerConstant

A deterministic (3.24) bound gives the exact squared geometric second-moment input used by the Cramér--Wold argument. All probabilistic qualitative premises are discharged by the concrete mollified-noise construction.

theorem Anderson4D.mainConditional_of_deterministic_bounds {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant Crenorm : ℝ} (houter : 0 < outerConstant) (hpower : 0 < powerConstant) (hCrenorm : 0 < Crenorm) (hdet : ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (hcounter : ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ q ∈ Finset.Icc 1 (truncOrder ε), |renormC2q ρ lam ε q| ≤ ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) : MainConditional M ρ

Final conditional theorem from the R-322 and R-324 quantitative estimates.