Numerical closure of the one-sided L² good-event budgets

This file records the elementary small-scale estimates which turn the explicit budgets in PerrLeftBoundaryMoment into the powers used in paper §3.4:

• the physical truncated-parametrix second moment is at most ε⁻²⁴;
• the left-boundary first moment is at most ε³⁰.

All constants are selected before the coupling and before the scale.

A scale-uniform Fourier-symbol sum

noncomputable def Anderson4D.PartialPairing.cutoffFourierDecayConstant (ρ : SmoothCutoff) : ℝ

A fixed eighth-order Schwartz constant for the cutoff.

Equations

• Anderson4D.PartialPairing.cutoffFourierDecayConstant ρ = Classical.choose ⋯

theorem Anderson4D.PartialPairing.cutoffFourierDecayConstant_pos (ρ : SmoothCutoff) : 0 < cutoffFourierDecayConstant ρ

theorem Anderson4D.PartialPairing.cutoffFourierDecayConstant_spec (ρ : SmoothCutoff) (ξ : R4) : (1 + ‖SmoothCutoff.euclideanFrequency ξ‖) ^ 8 * ‖fourierR4 ρ.toFun ξ‖ ≤ cutoffFourierDecayConstant ρ

noncomputable def Anderson4D.PartialPairing.cutoffSymbolSumConstant (ρ : SmoothCutoff) : ℝ

The fixed summability constant which appears after restricting the Schwartz multiplier to the lattice.

Equations

• Anderson4D.PartialPairing.cutoffSymbolSumConstant ρ = Anderson4D.PartialPairing.cutoffFourierDecayConstant ρ * (2 * Real.pi) ^ 8 * ∑' (k : Anderson4D.Z4), Anderson4D.latticeSummabilityWeight k

theorem Anderson4D.PartialPairing.cutoffSymbolSumConstant_pos (ρ : SmoothCutoff) : 0 < cutoffSymbolSumConstant ρ

theorem Anderson4D.PartialPairing.tsum_norm_symbol_le_cutoffSymbolSumConstant (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : ∑' (k : Z4), ‖ρ.symbol ε k‖ ≤ cutoffSymbolSumConstant ρ * ε⁻¹ ^ 8

Uniform polynomial control of the absolutely summable cutoff symbol. The power eight is deliberately wasteful but is fixed independently of the scale.

Exponential decay at the logarithmic truncation order

theorem Anderson4D.PartialPairing.exp_neg_nat_pow_truncOrder_le (N : ℕ) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : Real.exp (-↑N) ^ truncOrder ε ≤ Real.exp ↑N * ε ^ N

A fixed geometric ratio raised to ⌊|log ε|⌋ gives an arbitrary prescribed polynomial power of ε. The factor exp N is exactly the single unit lost by taking the floor.

theorem Anderson4D.PartialPairing.exp_neg_nat_pow_truncOrder_sub_one_le (N : ℕ) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (hA : 1 ≤ truncOrder ε) : Real.exp (-↑N) ^ (truncOrder ε - 1) ≤ Real.exp (2 * ↑N) * ε ^ N

One fewer geometric factor costs one further fixed exponential constant.

The physical second-moment budget

noncomputable def Anderson4D.PartialPairing.physicalSecondMomentConstant (outerConstant : ℝ) : ℝ

The scale- and order-independent part of the orderwise P-3.5b L² budget.

Equations

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

theorem Anderson4D.PartialPairing.physicalSecondMomentConstant_nonneg {outerConstant : ℝ} (houter : 0 ≤ outerConstant) : 0 ≤ physicalSecondMomentConstant outerConstant

theorem Anderson4D.PartialPairing.canonicalParametrixOrderL2SecondMomentBudget_le_coarse {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hratio : powerConstant * lam ≤ 1) (hlog : 1 ≤ |Real.log ε|) : canonicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m ≤ physicalSecondMomentConstant outerConstant * ε⁻¹ ^ 20

Once both the coupling and the geometric order ratio are at most one, every positive-order second moment is bounded by the same ε⁻²⁰ envelope.

theorem Anderson4D.PartialPairing.canonicalPhysicalTruncatedParametrixL2SecondMomentBudget_le_coarse {outerConstant powerConstant lam ε : ℝ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hratio : powerConstant * lam ≤ 1) (hε : 0 < ε) (hεle : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) : canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) ≤ 9 * (physicalSecondMomentConstant outerConstant + 1) * ε⁻¹ ^ 22

The moving physical finite sum admits a deliberately coarse ε⁻²² bound. This leaves two full powers for absorbing its fixed constant into the paper's ε⁻²⁴ threshold.

theorem Anderson4D.PartialPairing.eventually_canonicalPhysicalTruncatedParametrixL2SecondMomentBudget_le {outerConstant powerConstant lam : ℝ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hratio : powerConstant * lam ≤ 1) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) ≤ ε ^ (-24)

The physical budget eventually meets the exact power used in the Chebyshev threshold of paper (3.32).

Square-root envelopes for the boundary terms

noncomputable def Anderson4D.PartialPairing.physicalFirstMomentConstant (outerConstant : ℝ) : ℝ

Square root of the fixed P-3.5b second-moment constant.

Equations

• Anderson4D.PartialPairing.physicalFirstMomentConstant outerConstant = √(Anderson4D.PartialPairing.physicalSecondMomentConstant outerConstant)

theorem Anderson4D.PartialPairing.physicalFirstMomentConstant_nonneg (outerConstant : ℝ) : 0 ≤ physicalFirstMomentConstant outerConstant

theorem Anderson4D.PartialPairing.sqrt_canonicalParametrixOrderL2SecondMomentBudget_eq {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (hm : 1 ≤ m) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : √(canonicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m) = physicalFirstMomentConstant outerConstant * lamEps lam ε * (powerConstant * lam) ^ (m - 1) * ε⁻¹ ^ 10

Exact square-root factorization of the positive-order P-3.5b budget.

theorem Anderson4D.PartialPairing.sqrt_canonicalPhysicalParametrixOrderL2SecondMomentBudget_le {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (hm : 1 ≤ m) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hlog : 1 ≤ |Real.log ε|) : √(canonicalPhysicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m) ≤ physicalFirstMomentConstant outerConstant * (powerConstant * lam) ^ (m - 1) * ε⁻¹ ^ 10

Coarse positive-order square-root envelope after discarding the inverse-logarithmic gain in λ_ε.

noncomputable def Anderson4D.PartialPairing.noiseFirstMomentConstant (ρ : SmoothCutoff) : ℝ

Fixed constant in the square-root noise envelope.

Equations

• Anderson4D.PartialPairing.noiseFirstMomentConstant ρ = ‖Anderson4D.NoiseModel.whiteNoiseFourierScale‖ * Anderson4D.PartialPairing.cutoffSymbolSumConstant ρ

theorem Anderson4D.PartialPairing.noiseFirstMomentConstant_nonneg (ρ : SmoothCutoff) : 0 ≤ noiseFirstMomentConstant ρ

theorem Anderson4D.PartialPairing.sqrt_canonicalNoiseMultiplicationL2SecondMomentBudget_le (ρ : SmoothCutoff) {lam ε : ℝ} (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hε : 0 < ε) (hεle : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) : √(canonicalNoiseMultiplicationL2SecondMomentBudget ρ lam ε) ≤ noiseFirstMomentConstant ρ * ε⁻¹ ^ 8

Polynomial envelope for the degree-one noise multiplier.

Geometric routing in the boundary sum

noncomputable def Anderson4D.PartialPairing.boundaryGeometricRatio : ℝ

A deliberately tiny fixed ratio. Sixty-four powers of ε leave ample room for all polynomial losses in (3.32).

Equations

• Anderson4D.PartialPairing.boundaryGeometricRatio = Real.exp (-64)

theorem Anderson4D.PartialPairing.boundaryGeometricRatio_pos : 0 < boundaryGeometricRatio

theorem Anderson4D.PartialPairing.boundaryGeometricRatio_nonneg : 0 ≤ boundaryGeometricRatio

theorem Anderson4D.PartialPairing.boundaryGeometricRatio_le_one : boundaryGeometricRatio ≤ 1

theorem Anderson4D.PartialPairing.mul_order_pow_counterterm_pow_le_boundaryGeometricRatio {b c : ℝ} {A r q : ℕ} (hb0 : 0 ≤ b) (hb : b ≤ boundaryGeometricRatio) (hc0 : 0 ≤ c) (hc : c ≤ boundaryGeometricRatio) (hr : 1 ≤ r) (hroute : A < r + 2 * q) : b ^ (r - 1) * c ^ (2 * q) ≤ boundaryGeometricRatio ^ A

The routing inequality A < r + 2q turns the two perturbative ratios into at least A powers of the common geometric ratio.

theorem Anderson4D.PartialPairing.counterterm_pow_le_boundaryGeometricRatio {c : ℝ} {A q : ℕ} (hc0 : 0 ≤ c) (hc : c ≤ boundaryGeometricRatio) (hroute : A < 2 * q) : c ^ (2 * q) ≤ boundaryGeometricRatio ^ A

Order zero has no parametrix ratio, but the routing condition then puts all A geometric powers into the counterterm.

noncomputable def Anderson4D.PartialPairing.boundaryFirstMomentConstant (outerConstant : ℝ) (ρ : SmoothCutoff) : ℝ

Fixed coefficient in the final ε⁴⁶ boundary envelope.

Equations

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

theorem Anderson4D.PartialPairing.boundaryFirstMomentConstant_nonneg {outerConstant : ℝ} (ρ : SmoothCutoff) : 0 ≤ boundaryFirstMomentConstant outerConstant ρ

The boundary first-moment budget

theorem Anderson4D.PartialPairing.canonicalPerrLeftBoundaryFirstMomentBudget_le_coarse {outerConstant powerConstant Crenorm lam ε : ℝ} (ρ : SmoothCutoff) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hCrenorm : 0 ≤ Crenorm) (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hpowerRatio : powerConstant * lam ≤ boundaryGeometricRatio) (hrenormRatio : Crenorm * lam ≤ boundaryGeometricRatio) (hε : 0 < ε) (hεle : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) : (canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε (truncOrder ε) fun (q : ℕ) => ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) ≤ boundaryFirstMomentConstant outerConstant ρ * ε ^ 46

Under the paper's routing condition, sufficiently small fixed geometric ratios turn the entire finite boundary sum into O(ε⁴⁶). The exponent is deliberately stronger than the required 30.

theorem Anderson4D.PartialPairing.eventually_canonicalPerrLeftBoundaryFirstMomentBudget_le {outerConstant powerConstant Crenorm lam : ℝ} (ρ : SmoothCutoff) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hCrenorm : 0 ≤ Crenorm) (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hpowerRatio : powerConstant * lam ≤ boundaryGeometricRatio) (hrenormRatio : Crenorm * lam ≤ boundaryGeometricRatio) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), (canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε (truncOrder ε) fun (q : ℕ) => ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) ≤ ε ^ 30

The coarse ε⁴⁶ estimate eventually meets the exact ε³⁰ first-moment threshold of paper (3.32).

theorem Anderson4D.PartialPairing.exists_couplingThreshold_eventually_oneSidedBudgets {outerConstant powerConstant Crenorm : ℝ} (ρ : SmoothCutoff) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hCrenorm : 0 ≤ Crenorm) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (lam : ℝ), 0 ≤ lam → lam < lam0 → (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) ≤ ε ^ (-24)) ∧ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), (canonicalPerrLeftBoundaryFirstMomentBudget outerConstant powerConstant ρ lam ε (truncOrder ε) fun (q : ℕ) => ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) ≤ ε ^ 30

Coupling threshold chosen after the named deterministic constants but before λ and ε. Below this threshold both numerical budgets close simultaneously.

Final numerical good-event closure

theorem Anderson4D.PartialPairing.eventually_measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_two_mul_sq {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant Crenorm lam : ℝ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hCrenorm : 0 ≤ Crenorm) (hlam : 0 ≤ lam) (hlamle : lam ≤ 1) (hpowerRatio : powerConstant * lam ≤ boundaryGeometricRatio) (hrenormRatio : Crenorm * lam ≤ boundaryGeometricRatio) (hdet : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (hagree : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) (hcounter : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ q ∈ Finset.Icc 1 (truncOrder ε), |renormC2q ρ lam ε q| ≤ ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ 2 * ε ^ 2

Adapter from the moving deterministic P-3.5a/P-3.5b/P-3.4 inputs to the exact 2 ε² exceptional-set estimate. No numerical budget hypothesis remains.