RatioTailClosed

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

The 𝒢₀ lane: the anchor s-window of the per-atom tail

ABK26, §4.1, e.no.bad.scales.applied.for.lambdas for the 𝒢₀ lane.

• exp_le_budget and atomTail_of_budget — the abstract-real budget steps at E = C c⋆^{−1}.
• exists_cgExcess_atomTail_of_floor — the anchor s-window (hwin of AtomTail.exists_cgExcess_atomTail): exp(−(C_cg^{−1}E^{−2}γ^{−1})) ≤ γ/2 at the budget E = C c⋆^{−1}, from the printed regime γ ≤ C^{−10}c⋆^{10} for C(d) large; the per-atom Γ_{1/3} tail becomes unconditional.

Scope

Provider material: proved local helpers.

References

• ABK26, l.good.scales.ratio.lambda.

4. The two AtomTail bridges

5b. SLOT: the anchor's s-window at s = γ, discharged

theorem Algsuperdiff.Section4.Provider.Proportion.exists_cgExcess_atomTail_of_floor (d : ℕ) (C0 : ℝ) : ∃ (C : ℝ), 6 ≤ C ∧ C0 ≤ C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∃ (E : { E : ℝ // 1 ≤ E }), ↑E = C * (Section3.Disorder.cstar M)⁻¹ ∧ cgTailScale M ↑E ≤ M.gamma / 2 ∧ ∀ (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) (cgTailScale M ↑E)

The 𝒢₀ atom tail, unconditionally, at any floor the caller needs.

AtomTail.exists_cgExcess_atomTail delivers the per-atom Γ_{1/3} tail only under the anchor's own s-window premise hwin: exp(−(C_cg^{−1}E^{−2}γ^{−1})) ≤ γ/2, which it passes through as a caller obligation. That premise is the manuscript's own step and it is discharged here from the printed regime γ ≤ C^{−10}c⋆^{10} alone:

• at the budget E = C c⋆^{−1} the exponent is u = c⋆²/(C_cg C² γ), and the regime with the proved c⋆ ≤ 3/2 gives C⁶ ≤ 12 C_cg² γu² (regime_core);
• the floor C ≥ 6912 C_cg² therefore gives γu² ≥ 576, and exp(−u) ≤ 2/u² ≤ γ/2 (exp_neg_le_two_div_sq).

The extra floor is free for the caller (the p-choice needs its own).