RatioTailArith

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

The parameter arithmetic of the 𝒢₀ proportion tail

ABK26, §4.1, the three numerical steps of l.good.scales.ratio.lambda that the manuscript performs in one line each: the γ^{-4} normalizer, the regime bookkeeping behind the s-window of p.cg.ellipticity.bounds and behind the p-choice, and the threshold identification.

Everything here is abstract-real: no ABK carrier, no measure, no random variable. Per the elaboration discipline every transcendental atom (Real.exp, Real.log, Real.rpow) is confined to a dedicated helper and no numeric tactic ever sees one:

• exp_neg_le_factorial_div — exp(−w) ≤ n!/wⁿ, the single opening of the exponential, specialised at n = 2 and n = 7;
• one_sub_three_rpow_ge — 1 − 3^{−γ/4} ≥ γ/8, the spectral gap of the geometric weight;
• rpow_le_one_add — x^e ≤ 1 + x for e ∈ [0,1].

Main results

• tsum_weightThird_mul_annulusPenaltyThird_le — the γ^{-4} closed form Σ_j 3^{−¼γ j}(1 + d(j+3)log 3)³ ≤ penaltyNormalizer d · γ^{-4}, from the cubic penalty bound, Σ_j binom(j+3,3)wʲ = (1−w)^{-4} and the spectral gap.
• regime_core — the three power inequalities the printed regime γ ≤ C^{−10}c⋆^{10} yields for the atom-tail exponent u = c⋆²/(C_cg C² γ) at the budget E = C c⋆^{−1}, using the proved c⋆ ≤ 3/2.
• threshold_le_inv — the Appendix-D threshold 9 s'^{-1}C^{1/p}θ^{-1/p} sits below D^{-1} as soon as 9 D (1 + C_⋆) ≤ s' θ.
• exists_dependence_range — an r ≥ 1 with 3 + (2/3)√d ≤ 3^r exists in every dimension.

Scope

Provider material: proved local helpers.

References

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

1. Abstract-real transcendental helpers

theorem Algsuperdiff.Section4.Provider.Proportion.exp_neg_le_two_div_sq {w : ℝ} (hw : 0 < w) : Real.exp (-w) ≤ 2 / w ^ 2

exp(−w) ≤ 2/w².

theorem Algsuperdiff.Section4.Provider.Proportion.exp_neg_le_seven {w : ℝ} (hw : 0 < w) : Real.exp (-w) ≤ 5040 / w ^ 7

exp(−w) ≤ 5040/w⁷.

2. The γ^{-4} closed form of the 𝒴-normalizer

noncomputable def Algsuperdiff.Section4.Provider.Proportion.penaltyNormalizer (d : ℕ) : ℝ

The dimensional constant of the 𝒴-normalizer. With it, Σ_j 3^{−¼γ j}(1+d(j+3)log 3)³ ≤ penaltyNormalizer d · γ^{-4}, which is the manuscript's γ^{-4} in closed form (: the normalization is a lane prefactor, so this is a bound on the tail scale, not a rescaling of the score field).

Equations

• Algsuperdiff.Section4.Provider.Proportion.penaltyNormalizer d = 24576 * (1 + 3 * ↑d * Real.log 3) ^ 3

theorem Algsuperdiff.Section4.Provider.Proportion.penaltyNormalizer_pos (d : ℕ) : 0 < penaltyNormalizer d

theorem Algsuperdiff.Section4.Provider.Proportion.tsum_weightThird_mul_annulusPenaltyThird_le (d : ℕ) {gamma : ℝ} (h0 : 0 < gamma) (h4 : gamma ≤ 1 / 4) : ∑' (j : ℕ), weightThird (gamma / 4) j * annulusPenaltyThird d (j + 2) ≤ penaltyNormalizer d / gamma ^ 4

The γ^{-4} closed form. The weighted lattice penalties of the 𝒴-tail sum to at most penaltyNormalizer d · γ^{-4} at the manuscript's rate s' = γ/4. The three ingredients are the cubic penalty bound, the identity Σ_j binom(j+3,3) w^j = (1−w)^{-4}, and the spectral gap 1 − 3^{−γ/4} ≥ γ/8.

3. The regime core: two power inequalities

theorem Algsuperdiff.Section4.Provider.Proportion.regime_core {gamma cs Ccg C u : ℝ} (hg : 0 < gamma) (hcs : 0 < cs) (hcs32 : cs ≤ 3 / 2) (hCcg : 0 < Ccg) (hC : 0 < C) (hreg : gamma ≤ C⁻¹ ^ 10 * cs ^ 10) (hu : u = Ccg⁻¹ * (C * cs⁻¹)⁻¹ ^ 2 * gamma⁻¹) : C ^ 6 ≤ 12 * Ccg ^ 2 * (gamma * u ^ 2) ∧ C ^ 6 ≤ 12 * Ccg ^ 7 * (gamma ^ 5 * u ^ 7) ∧ C ^ 4 ≤ 6 * Ccg ^ 3 * (gamma ^ 2 * u ^ 3)

The abstract-real core of the parameter arithmetic. With the atom-tail exponent u = c⋆²/(C_cg C² γ) at the budget E = C c⋆^{−1}, the printed regime γ ≤ C^{−10}c⋆^{10} and the proved c⋆ ≤ 3/2 give the two lower bounds the s-window and the p-choice consume. No transcendental atom appears.

5. The threshold identification

theorem Algsuperdiff.Section4.Provider.Proportion.threshold_le_inv {sprime theta p D : ℝ} (hs : 0 < sprime) (ht0 : 0 < theta) (ht1 : theta ≤ 1) (hp : 1 ≤ p) (hD : 0 < D) (hkey : 9 * D * (1 + Probability.ScalesConcentration.Cstar) ≤ sprime * theta) : 9 * sprime⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p) ≤ D⁻¹

The Appendix-D threshold sits below D^{-1}. The manuscript's threshold identification: C^{1/p} ≤ 1 + C and θ^{-1/p} ≤ θ^{-1} for p ≥ 1 and θ ∈ (0,1], so the whole level is controlled by the single inequality 9 D (1 + C_⋆) ≤ s' θ.

6. The dependence range

theorem Algsuperdiff.Section4.Provider.Proportion.exists_dependence_range (d : ℕ) : ∃ (r : ℕ), 1 ≤ r ∧ 3 + 2 * 3 ^ (1 - 2) * √↑d ≤ 3 ^ r