Final conditional-theorem assembly

This file records the exact interfaces still supplied by the coefficient second-moment estimate and the operator good-event argument, then performs all remaining quantifier, coupling-threshold, filter, and characteristic-function bookkeeping for Theorem 1.1.

Neither interface assumes convergence in law or a characteristic-function limit. MainSecondMomentInput is precisely the squared geometric form of paper (3.24), while FixedModeGoodEventData is the direct fixed-mode replacement output of paper §3.4 Steps 1--2.

def Anderson4D.MainSecondMomentInput (M : NoiseModel) (ρ : SmoothCutoff) (K powerConstant : ℝ) : Prop

Uniform squared geometric coefficient control in the form consumed by the moving-truncation theorem. The constants are selected before the coupling and the finite family of Fourier modes.

Equations

• One or more equations did not get rendered due to their size.

structure Anderson4D.FixedModeGoodEventData (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Type

Fixed-mode output of the operator comparison on its measurable good event. It is intentionally quantitative and contains no limiting-law statement.

• good : ℝ → Set M.Ω
• error : ℝ → ℝ
• good_measurable (ε : ℝ) : MeasurableSet (self.good ε)
• error_nonneg : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 ≤ self.error ε
• error_tendsto : Filter.Tendsto self.error (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
• bad_probability_tendsto : Filter.Tendsto (fun (ε : ℝ) => MeasureTheory.volume.real (self.good ε)ᶜ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
• close_on_good : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ ω ∈ self.good ε, ‖fullParametrixReal M ρ lam ε s modes c ω - fullResolventReal M ρ lam ε s modes c ω‖ ≤ self.error ε

def Anderson4D.MainGoodEventInput (M : NoiseModel) (ρ : SmoothCutoff) : Prop

Uniform availability of the fixed-mode good-event comparison.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.mainConditional_of_secondMoment_and_goodEvent {M : NoiseModel} {ρ : SmoothCutoff} {K powerConstant : ℝ} (hK : 0 ≤ K) (hpower : 0 < powerConstant) (hsecond : MainSecondMomentInput M ρ K powerConstant) (hgood : MainGoodEventInput M ρ) : MainConditional M ρ

Complete quantifier assembly for the conditional main theorem.

Given the genuine upstream outputs of (3.24) and the operator good-event comparison, the external Proposition 3.6 family implies the frozen main statement. The coupling threshold is the minimum of the independent external and internal geometric thresholds.