Final assembly from deterministic estimates

This module removes the abstract MainGoodEventInput interface. Given the moving deterministic P-3.5b estimate and the R-322 counterterm estimate, the measurable event is constructed internally and the characteristic-function argument is completed at one common coupling threshold.

theorem Anderson4D.mainConditional_of_secondMoment_and_deterministic_bounds {M : NoiseModel} {ρ : SmoothCutoff} {K secondPower outerConstant goodPower Crenorm : ℝ} (hK : 0 ≤ K) (hsecondPower : 0 < secondPower) (houter : 0 ≤ outerConstant) (hgoodPower : 0 < goodPower) (hCrenorm : 0 < Crenorm) (hsecond : MainSecondMomentInput M ρ K secondPower) (hdet : ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant goodPower 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 ρ

Complete quantifier assembly from the second-moment estimate and the two deterministic inputs to the one-sided operator good event.