G2ThresholdSharp #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The 𝒢₂ proportion endpoint at the θ-free ε-threshold #
G2Threshold.ratioTail_eventG2_of_threshold_shift restates the proved lane at
the named threshold g2Threshold … = 36(1+C⋆)D/θ. This module restates it at
the sharp threshold g2ThresholdSharp … = 108(1+C⋆)D, which carries no
divisor θ: the quantile factor θ^{-1/p} is paid logarithmically
(G2SharpArith.threshold_le_inv_sharp) rather than by θ^{-1/p} ≤ θ^{-1}, and
the lane's own moment exponent already clears the requirement θ⁻¹ ≤ p
(G2SharpArith.inv_theta_le_g2MomentExponent).
Nothing else in the lane changes: the moment exponent, the normalizer, the independence geometry, the per-cube display and the reduction are the proved ones, character for character.
Contents #
ratioTail_eventG2_of_thresholdSharp_shift— the explicit-threshold endpoint atg2ThresholdSharp, in theLaneTailFromshape the proportion assembly consumes;g2SharpAnchorConst,g2SharpAnchorConstTwo— twod-only constants;g2ThresholdSharp_le_of_anchor_rate/_solved/g2ThresholdSharp_le_of_anchor— the threshold condition at the frozen proportion anchor's own parameter ranges, its regime clause and itss⁻⁶level clause, at the assembly ratec₁ = 2A.
The headline #
At the anchor's own clauses the sharp threshold condition reduces to the two parameter-free constant floors
g2SharpAnchorConst d r C N ≤ C_a and g2SharpAnchorConstTwo d r C N ≤ C_a ,
both functions of d alone. There is no new anchor clause: in particular
nothing of the shape C_aθ ≥ κ(d)s that the proved
G2Threshold.g2Threshold_le_of_anchor needed. The anchor's own level clause
C_a c⋆^{-2}s^{-6}ε^{-2}γ ≤ θ does all the work, because the sharp threshold's
binding clause carries only one power of θ on its favourable side, and the
level clause supplies exactly one.
Scope #
Provider material: proved local helpers. The ε-threshold condition of the
endpoint is a genuine hypothesis of the lane, not a source premise smuggled
into a frozen statement, and the two constant floors are explicit named
parameter conditions.
References #
- ABK26,
l.ratio.of.good.scales.for.mathcal.E;p.concentration.for.scales.
1. The endpoint at the θ-free threshold #
This is the shifted 𝒢₂ lane endpoint with its existential threshold
∃ ε₀ > 0, ∀ ε ≥ ε₀ replaced by the named condition
0 < ε and g2ThresholdSharp d r C M s θ c₁ ≤ ε² ,
g2ThresholdSharp … = 108(1+C⋆)·D being a closed-form expression in the lane's parameters
with no divisor θ (contrast g2Threshold … = 36(1+C⋆)D/θ). Every other hypothesis
is that of the proved endpoint, unchanged: the honest range condition, the printed regime
γ ≤ C^{−10}c⋆^{10}, the standing window s ∈ [8γ,1], the level condition θ(r+1) < 1
and c₁ ≥ 0. The base m₀ and the window n are quantified last, so the conclusion is
the LaneTailFrom shape the proportion assembly consumes.
2. The sharp threshold at the frozen theorem's own parameters #
Unlike its proved counterpart G2Threshold.g2AnchorConst, this constant is
asked to clear C_a outright: the anchor-side condition is
g2SharpAnchorConst d r ≤ C_a, with no s and no θ in it.
Equations
Instances For
The constant-size floor the anchor's own constant must clear so that the
exponentially small clause of the sharp threshold condition is free. Like
g2SharpAnchorConst it constrains only C_a against d.
Equations
Instances For
The sharp threshold condition at the anchor's clauses, for an arbitrary rate.
The rate enters only through hZ, the requirement that γ(1+c₁) still obeys
the anchor's level clause up to a factor 2. Everything else is the anchor's
own data: its parameter ranges s, ε, θ ∈ (0,½], its regime clause γ ≤ C_a^{-1}c⋆^{10}, its s⁻⁶ level clause in solved form hlev, and the two
parameter-free constant floors hkappa, hCaBig.
This is the item-9 payoff: compare G2Threshold.g2Threshold_le_of_anchor_rate,
whose corresponding hypothesis is g2AnchorConst d r · s ≤ C_a · θ — a genuine
new clause coupling θ to s, which the verified consumer refutes. Here
there is no such clause at all.
The sharp threshold condition at the assembly rate c₁ = 2A, from the
level clause in solved form.
A = c⋆²s⁷ε²θ/(C_aγ) is the rate the anchor clause carries. The grouping
γ(1+c₁) = γ + 2sX, X = θc⋆²s⁶ε²/C_a, linearises the requirement at once: γ ≤ X and 2s ≤ 1 give γ(1+c₁) ≤ 2X.
The lane is read at level θ/N and at the assembly rate c₁ = 2A, A = c⋆²s⁷ε²θ/(C_aγ). Under the anchor's parameter ranges, its regime clause and
its s⁻⁶ level clause, the whole ε-threshold condition reduces to the two
parameter-free constant floors
g2SharpAnchorConst d r C N ≤ C_a and g2SharpAnchorConstTwo d r C N ≤ C_a ,
both functions of d alone (once the lane's range r(d), its constant C(d)
and the level divisor N are fixed). There is no residual clause in
θ or s.
This resolves the 𝒢₂ side: the proved
G2Threshold.g2Threshold_le_of_anchor needed g2AnchorConst d r · s ≤ C_aθ,
which the verified consumer refutes as θ → 0; the log-quantile reading
removes it entirely.