G1ThresholdArith #

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

An explicit majorant for the `𝒢₁` proportion threshold #

The 𝒢₁ proportion tail is delivered at an existential, unexposed threshold T₀, and only at the dependence range r = 1. This module replaces that existential by an explicit closed form, valid at every r ≥ 1:

g1ThresholdConst d r — a positive constant depending only on d and r (through Cstar, gammaMomentConst, atomG1bScale and log 3);
g1Majorant d r s θ c₁ = √(g1ThresholdConst d r (1+c₁) / (s⁴ θ));
g1Majorant_le_shellThreshold — the certificate that this majorant sits below the threshold at which the Section 4 support layer instantiates 𝒢₁.

The honest reading of the threshold condition #

g1Majorant_le_shellThreshold certifies that this majorant sits below the threshold T = s ε √(c⋆) (√γ)⁻¹ at which the Section 4 support layer instantiates 𝒢₁ inside Support.goodEventBase, under the explicit condition

K(d,r) (1 + c₁) γ ≤ θ c⋆ s⁶ ε²          (`hcond`)

which is exactly T₀² ≤ (s ε)² c⋆ γ⁻¹ written out. Measured against the manuscript's printed side condition e.theta.cond.two (T² ≥ C s^{-2} max{s^{-1}, θ^{-1}}), hcond is one power of s^{-2} stronger: the printed condition would read s⁴ where hcond needs s⁶. Nothing in this module consumes the printed condition, and no declaration here claims a source node, or any fraction of one, closed.

References #

ABK26, l.ratio.of.good.scales.for.k, Step 3.
ABK26, d.good.event.for.lambda, (the 𝒢₁ threshold s ε c⋆^{1/2} γ^{-1/2}).

1. Abstract-real helpers #

Every transcendental atom (Real.exp, Real.log, Real.rpow, Real.sqrt) is confined to this section; the closed-form arithmetic below sees only opaque reals.

3. The explicit threshold constant and majorant #

source

noncomputable def Algsuperdiff.Section4.Provider.Proportion.g1ThresholdConst (d r : ℕ) :

ℝ

The d- and r-only prefactor of the closed 𝒢₁ threshold. The first summand carries the large-waves lane (54² · 66 times the squared Appendix-D normaliser), the second the small-waves lane (24 · 216 · 8 · 262 times the Γ₁ amplitude of the two-index array).

Equations