LambdaWindow

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The s-window of p.cg.ellipticity.bounds at s = γ, discharged

The obligation this module removes

Proportion.exists_cgExcess_atomTail and the (B5) statements of LambdaSlotB5.lean carry ONE undischarged premise, the anchor's own s-window read at s = γ:

cgTailScale M E = exp(−(C_cg^{−1} E^{−2} γ^{−1}))  ≤  γ/2 .

This module formalizes that note at the budget E = C c⋆^{−1} actually supplied, in the anchor's OWN regime γ ≤ C^{−10} c⋆^{10}.

The arithmetic, in full

Write r := c⋆/C, so that E^{−1} = r and the regime reads γ ≤ r^{10}. With K := C_{(e.cg.ellip.lower)} and S := √(γ^{−1}) ≥ 1:

• S ≥ r^{−5} (square both sides of γ ≤ r^{10});
• K^{−1} r² γ^{−1} = (K^{−1} r² S) S ≥ (K^{−1} r^{−3}) S ≥ 3 S, the last step being exactly the hypothesis 3 K r³ ≤ 1;
• log(2/γ) = log 2 + log(S²) ≤ 1 + 2(S − 1) ≤ 3S.

Hence K^{−1} r² γ^{−1} ≥ log(2/γ), which is the window. The hypothesis 3 K r³ ≤ 1 is met by ANY constant C ≥ max{6, K}: c⋆ ≤ 3/2 gives r ≤ (3/2)C^{−1}, so 3 K r³ ≤ (81/8) K C^{−3}, and C ≥ 6 gives C³ ≥ 36 C ≥ 36 K ≥ (81/8) K. No γ-exponent and no s-power is moved: the regime and the amplitude are the printed ones.

Only natural powers, Real.sqrt, Real.log and Real.exp appear; every transcendental atom is kept opaque (no nlinarith anywhere).

References

• ABK26, p.cg.ellipticity.bounds, (the s-range).

1. The abstract-real window

2. The amplitude is monotone in the budget E

theorem Algsuperdiff.Section4.Provider.BoundsEaL.cgTailScale_mono {d : ℕ} (M : Section3.ABKModel d) {E E' : ℝ} (hE : 0 < E) (hEE : E ≤ E') : Proportion.cgTailScale M E ≤ Proportion.cgTailScale M E'

The Orlicz amplitude exp(−C_cg^{−1}E^{−2}γ^{−1}) is nondecreasing in the budget E: a larger E is a weaker conclusion.

3. The window at the anchor's own budget and regime

theorem Algsuperdiff.Section4.Provider.BoundsEaL.cgTailScale_le_half_gamma {d : ℕ} (M : Section3.ABKModel d) {C : ℝ} (hC6 : 6 ≤ C) (hCcg : Support.cgEllipLowerConstant d ≤ C) (hreg : M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10) : Proportion.cgTailScale M (C * (Section3.Disorder.cstar M)⁻¹) ≤ M.gamma / 2

hwin, discharged. At the budget E = C c⋆^{−1} and in the anchor's own regime γ ≤ C^{−10} c⋆^{10}, the s-window at s = γ holds for every constant C ≥ max{6, C_{(e.cg.ellip.lower)}}.

4. The atom tail, unconditional in the anchor's regime

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_cgExcess_atomTail_unconditional (d : ℕ) : ∃ (C : ℝ), 6 ≤ C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∃ (E : { E : ℝ // 1 ≤ E }), ↑E = C * (Section3.Disorder.cstar M)⁻¹ ∧ ∀ (k : ℤ) (z : HCPolySupport.Vec d), HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (1 / 3)) (fun (omega : Section3.Cutoff.CutoffSample d) => Localize.cgExcess M (Support.cgEllipLowerConstant d) (k - 2) z omega) (Proportion.cgTailScale M ↑E)

Proportion.exists_cgExcess_atomTail with its hwin premise removed.

There is a dimensional constant C such that every model in the printed regime γ ≤ C^{−10}c⋆^{10} has, at the budget E = C c⋆^{−1}, for every k ∈ ℤ and every real centre z,

( σ_{k−3} λ_{γ,2}^{-1}(z+□_{k−2}; 𝐚_{k−2}) − C_{(e.cg.ellip.lower)} )_+
  ≤ 𝒪_{Γ_{1/3}} ( exp(−(C_cg C²)^{−1} c⋆² γ^{−1}) ) ,

with NO remaining hypothesis. The constant is the proved one raised to C_{(e.cg.ellip.lower)}, which is what makes the window self-discharging.