First-moment bound for the one-sided parametrix boundary

This file closes the elementary probabilistic part of paper (3.32). The last-block boundary from (3.21) is first identified almost surely with a measurable finite sum of the physical coefficient operators. Cauchy--Schwarz then reduces its first moment to the orderwise P-3.5b second-moment bounds, the continuous-noise second moment, and the P-3.5a bounds on the deterministic counterterms.

The zeroth physical order is kept separate: it is the bounded Green operator, not a Hilbert--Schmidt coefficient operator.

A measurable physical representative of each graded order

noncomputable def Anderson4D.PartialPairing.canonicalPhysicalParametrixOrderL2Operator (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

The physical order P_m = Q_m G. At order zero this is G; positive orders use the canonical Fourier-coefficient realization.

Equations

• Anderson4D.PartialPairing.canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω = if m = 0 then Anderson4D.greenL2Op else Anderson4D.canonicalParametrixOrderL2Operator M ρ lam ε m ω

noncomputable def Anderson4D.PartialPairing.canonicalPhysicalParametrixOrderL2SecondMomentBudget (outerConstant powerConstant lam ε : ℝ) (m : ℕ) : ℝ

Its second-moment budget, with the deterministic zeroth order bounded by one.

Equations

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

theorem Anderson4D.PartialPairing.canonicalPhysicalParametrixOrderL2SecondMomentBudget_nonneg {outerConstant powerConstant lam ε : ℝ} (m : ℕ) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : 0 ≤ canonicalPhysicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_mul_green_eq_physical (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A m : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (hm : m ≤ A) (hagree : ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hcanonical : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalParametrixOrderL2Operator M ρ lam ε n ω) α β = (↑paperTorusVolume)⁻¹ * pmCoeff M ρ lam ε n α β ω) : gradedParametrixL2FactorOrder M ρ lam ε ω hξ m * greenL2Op = canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω

Measurable noise and counterterm multipliers

noncomputable def Anderson4D.PartialPairing.canonicalNoiseMultiplicationL2Operator (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

The measurable degree-one multiplier.

Equations

• Anderson4D.PartialPairing.canonicalNoiseMultiplicationL2Operator M ρ lam ε ω = Anderson4D.continuousMultiplicationOp (↑(Anderson4D.lamEps lam ε) • Anderson4D.xiEpsContinuousMap M ρ ε ω)

noncomputable def Anderson4D.PartialPairing.canonicalCountertermMultiplicationL2Operator (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

Multiplication by the deterministic order-2q counterterm.

Equations

• Anderson4D.PartialPairing.canonicalCountertermMultiplicationL2Operator ρ lam ε q = Anderson4D.continuousMultiplicationOp (ContinuousMap.const Anderson4D.T4 ↑(Anderson4D.renormC2q ρ lam ε q))

theorem Anderson4D.PartialPairing.renormWordWeightContinuousMap_one_eq (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (hsum : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) : renormWordWeightContinuousMap M ρ lam ε ω hξ 1 = ↑(lamEps lam ε) • xiEpsContinuousMap M ρ ε ω

theorem Anderson4D.PartialPairing.gradedNoiseL2Factor_eq_measurable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (hsum : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) : gradedNoiseL2Factor M ρ lam ε ω hξ = greenL2Op * canonicalNoiseMultiplicationL2Operator M ρ lam ε ω

theorem Anderson4D.PartialPairing.gradedCountertermL2Factor_eq_measurable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (q : ℕ) : gradedCountertermL2Factor M ρ lam ε ω hξ q = greenL2Op * canonicalCountertermMultiplicationL2Operator ρ lam ε q

The measurable physical boundary

noncomputable def Anderson4D.PartialPairing.measurableCanonicalPerrLeftBoundary (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

Measurable physical realization of the last-block boundary in (3.21).

Equations

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

theorem Anderson4D.PartialPairing.gradedPerrLeftBoundary_eq_measurable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (hsum : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (hagree : ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hcanonical : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalParametrixOrderL2Operator M ρ lam ε n ω) α β = (↑paperTorusVolume)⁻¹ * pmCoeff M ρ lam ε n α β ω) : gradedPerrLeftBoundary M ρ lam ε ω hξ A = measurableCanonicalPerrLeftBoundary M ρ lam ε A ω

theorem Anderson4D.PartialPairing.ae_canonicalPerrLeftBoundary_eq_measurable {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ A → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) : canonicalPerrLeftBoundary M ρ lam ε A =ᵐ[MeasureTheory.volume] measurableCanonicalPerrLeftBoundary M ρ lam ε A

Measurability and L² control of the physical pieces

theorem Anderson4D.PartialPairing.aestronglyMeasurable_canonicalPhysicalParametrixOrderL2Operator {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : MeasureTheory.AEStronglyMeasurable (canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m) MeasureTheory.volume

theorem Anderson4D.PartialPairing.integrable_normSq_canonicalPhysicalParametrixOrderL2Operator {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω‖ ^ 2) MeasureTheory.volume

theorem Anderson4D.PartialPairing.memLp_canonicalPhysicalParametrixOrderL2Operator {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : MeasureTheory.MemLp (canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m) 2 MeasureTheory.volume

theorem Anderson4D.PartialPairing.integral_normSq_canonicalPhysicalParametrixOrderL2Operator_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∫ (ω : M.Ω), ‖canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω‖ ^ 2 ≤ canonicalPhysicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m

The measurable degree-one multiplier

theorem Anderson4D.PartialPairing.measurable_canonicalNoiseMultiplicationL2Operator (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable (canonicalNoiseMultiplicationL2Operator M ρ lam ε)

noncomputable def Anderson4D.PartialPairing.canonicalNoiseMultiplicationL2SecondMomentBudget (ρ : SmoothCutoff) (lam ε : ℝ) : ℝ

Explicit second-moment budget for the degree-one multiplication operator.

Equations

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

theorem Anderson4D.PartialPairing.canonicalNoiseMultiplicationL2SecondMomentBudget_nonneg (ρ : SmoothCutoff) (lam ε : ℝ) : 0 ≤ canonicalNoiseMultiplicationL2SecondMomentBudget ρ lam ε

theorem Anderson4D.PartialPairing.memLp_canonicalNoiseMultiplicationL2Operator (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.MemLp (canonicalNoiseMultiplicationL2Operator M ρ lam ε) 2 MeasureTheory.volume

theorem Anderson4D.PartialPairing.integral_normSq_canonicalNoiseMultiplicationL2Operator_le (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : ∫ (ω : M.Ω), ‖canonicalNoiseMultiplicationL2Operator M ρ lam ε ω‖ ^ 2 ≤ canonicalNoiseMultiplicationL2SecondMomentBudget ρ lam ε

Cauchy--Schwarz estimates for the boundary summands

theorem Anderson4D.PartialPairing.integral_norm_physicalParametrixOrder_mul_noise_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∫ (ω : M.Ω), ‖canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω * canonicalNoiseMultiplicationL2Operator M ρ lam ε ω‖ ≤ √(canonicalPhysicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m) * √(canonicalNoiseMultiplicationL2SecondMomentBudget ρ lam ε)

theorem Anderson4D.PartialPairing.integral_norm_physicalParametrixOrder_mul_counterterm_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (q : ℕ) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∫ (ω : M.Ω), ‖canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω * canonicalCountertermMultiplicationL2Operator ρ lam ε q‖ ≤ √(canonicalPhysicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m) * |renormC2q ρ lam ε q|

Integrability and finite-sum bookkeeping

theorem Anderson4D.PartialPairing.integrable_physicalParametrixOrder_mul_noise {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : MeasureTheory.Integrable (fun (ω : M.Ω) => canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω * canonicalNoiseMultiplicationL2Operator M ρ lam ε ω) MeasureTheory.volume

theorem Anderson4D.PartialPairing.integrable_physicalParametrixOrder_mul_counterterm {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A m : ℕ} (hm : m ≤ A) (q : ℕ) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : MeasureTheory.Integrable (fun (ω : M.Ω) => canonicalPhysicalParametrixOrderL2Operator M ρ lam ε m ω * canonicalCountertermMultiplicationL2Operator ρ lam ε q) MeasureTheory.volume

theorem Anderson4D.PartialPairing.integrable_measurableCanonicalPerrLeftBoundary {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : MeasureTheory.Integrable (measurableCanonicalPerrLeftBoundary M ρ lam ε A) MeasureTheory.volume

theorem Anderson4D.PartialPairing.integrable_canonicalPerrLeftBoundary {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) : MeasureTheory.Integrable (canonicalPerrLeftBoundary M ρ lam ε A) MeasureTheory.volume

Explicit first-moment budget

noncomputable def Anderson4D.PartialPairing.canonicalPerrLeftBoundaryFirstMomentBudget (outerConstant powerConstant : ℝ) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (countertermBudget : ℕ → ℝ) : ℝ

The finite expression obtained from P-3.5b, the continuous-noise second moment, and a supplied P-3.5a envelope for |C_{2q}|.

Equations

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

theorem Anderson4D.PartialPairing.integral_norm_canonicalPerrLeftBoundary_le_budget {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (countertermBudget : ℕ → ℝ) (hfubini : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε n α β) (hwick : ∀ (n : ℕ), 1 ≤ n → n ≤ A → WickAtSecondMomentLaw M ρ ε n) (hdet : ∀ (n : ℕ), 1 ≤ n → n ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε n α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε n α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hcounter : ∀ q ∈ Finset.Icc 1 A, |renormC2q ρ lam ε q| ≤ countertermBudget q) : ∫ (ω : M.Ω), ‖canonicalPerrLeftBoundary M ρ lam ε A ω‖ ≤ canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε A countertermBudget

The concrete one-sided event estimate

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_budget {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} (countertermBudget : ℕ → ℝ) (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) (hcounter : ∀ q ∈ Finset.Icc 1 (truncOrder ε), |renormC2q ρ lam ε q| ≤ countertermBudget q) : MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) / (ε ^ (-14)) ^ 2 + canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε (truncOrder ε) countertermBudget / ε ^ 28

The one-sided good-event probability with both former boundary interfaces discharged by the explicit first-moment theorem above.

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_of_deterministic {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} (countertermBudget : ℕ → ℝ) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) (hcounter : ∀ q ∈ Finset.Icc 1 (truncOrder ε), |renormC2q ρ lam ε q| ≤ countertermBudget q) : MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) / (ε ^ (-14)) ^ 2 + canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε (truncOrder ε) countertermBudget / ε ^ 28

The qualitative P-3.5b inputs in the preceding theorem are constructive consequences of the mollified-noise model. Only the quantitative deterministic moment estimate remains.

theorem Anderson4D.PartialPairing.exists_measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_of_reductions {M : NoiseModel} {ρ : SmoothCutoff} {primitiveConstant supportConstant outerConstant powerConstant lam ε : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hred : ∀ q ∈ Finset.Icc 1 (truncOrder ε), RenormReductionOutput ρ lam ε q primitiveConstant supportConstant) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) : ∃ (Crenorm : ℝ), 0 < Crenorm ∧ MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) / (ε ^ (-14)) ^ 2 + (canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε (truncOrder ε) fun (q : ℕ) => ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) / ε ^ 28

R-322 supplies the counterterm envelope in the exact form consumed by the boundary budget, with one constant selected before q.

theorem Anderson4D.PartialPairing.exists_measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_of_r322_r324 {M : NoiseModel} {ρ : SmoothCutoff} {renormPrimitive renormSupport momentPrimitive momentSupport lam ε : ℝ} (hrenormPrimitive : 0 < renormPrimitive) (hrenormSupport : 0 < renormSupport) (hmomentPrimitive : 0 < momentPrimitive) (hmomentSupport : 0 < momentSupport) (hrenorm : ∀ q ∈ Finset.Icc 1 (truncOrder ε), RenormReductionOutput ρ lam ε q renormPrimitive renormSupport) (huniform : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), MomentUniformReductionOutputAt ρ lam ε m α β momentPrimitive momentSupport) (hrouted : ∀ (outerConstant : ℝ), 0 < outerConstant → ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), RoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (momentPrimitive * lam) ^ (2 * m - 2))) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlog : 1 ≤ |Real.log ε|) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) : ∃ (outerConstant : ℝ) (Crenorm : ℝ), 0 < outerConstant ∧ 0 < Crenorm ∧ MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant momentPrimitive lam ε (truncOrder ε) / (ε ^ (-14)) ^ 2 + (canonicalPerrLeftBoundaryFirstMomentBudget outerConstant momentPrimitive ρ lam ε (truncOrder ε) fun (q : ℕ) => ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) / ε ^ 28

Complete event/first-moment assembly from the literal quantitative R-322 and R-324 outputs. All qualitative P-3.5b, Wick, boundary integrability, and abstract first-moment premises have disappeared. The only P-3.4 input left is hagree.

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_two_mul_sq_of_budgets {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} (countertermBudget : ℕ → ℝ) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hphysical : canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) ≤ ε ^ (-24)) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) (hcounter : ∀ q ∈ Finset.Icc 1 (truncOrder ε), |renormC2q ρ lam ε q| ≤ countertermBudget q) (hboundary : canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε (truncOrder ε) countertermBudget ≤ ε ^ 30) : MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ 2 * ε ^ 2

Paper-scale numerical budgets now imply the exact 2 ε² exceptional-set estimate without any separate boundary integrability or first-moment hypotheses.