G1RatioTail

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

Sign facts for the Appendix-D threshold of the 𝒢₁ lane

ABK26, §4.1, l.ratio.of.good.scales.for.k, Step 3, splits a θ-density of 𝒢₁-bad scales into a θ/2-density for one of the two lanes eventG1a, eventG1b. What this module keeps are the two sign facts that step consumes:

• half_le_one_sub_gamma — the standing assumption γ ≤ 1/4 of ShellLawPrefix makes the large-waves Appendix-D weight rate s' = 1/2 admissible;
• appendixD_level_nonneg — the Appendix-D threshold level is nonnegative, the hlam slot of both lanes' reductions.

References

• ABK26, l.ratio.of.good.scales.for.k, Step 3.
• ABK26, d.good.event.for.lambda.

1. Sign facts for the Appendix-D threshold

theorem Algsuperdiff.Section4.Provider.Proportion.half_le_one_sub_gamma {d : ℕ} (M : Section3.ABKModel d) : 1 / 2 ≤ 1 - M.gamma

The standing assumption γ ≤ 1/4 of ShellLawPrefix makes the large-waves Appendix-D weight rate s' = 1/2 admissible: 1/2 ≤ 1 - γ.

theorem Algsuperdiff.Section4.Provider.Proportion.appendixD_level_nonneg {sprime p theta : ℝ} (hs : 0 < sprime) (htheta : 0 < theta) : 0 ≤ 9 * sprime⁻¹ * Probability.ScalesConcentration.Cstar ^ (1 / p) * theta ^ (-1 / p)

The Appendix-D threshold level is nonnegative — the hlam slot of both lanes' reductions.