LaneCertificates

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

The frozen-anchor bridge arithmetic of the two lane couplings

ABK26, §4.1. The 𝒢₀ and 𝒢₁ ratio-tail lanes are unconditional in everything probabilistic; what each still needs is one explicit inequality tying the model to the level θ and the rate c₁:

• 𝒢₀: C⁹γ² ≤ θ c⋆⁸ — the level-vs-regime coupling that replaces the proved RatioTailClosed packaging of θ inside the constant (couplingG0_of_anchor);
• 𝒢₁: K(d,r)(1+c₁)γ ≤ θ c⋆ s⁶ ε² — the closed form of T₀ ≤ s ε √c⋆ γ^{-1/2} at the substituted threshold of e.lambda.good.events (couplingG1_of_anchor).

Both are abstract-real implications recording what the frozen proportion anchor's own parameter clauses give. The anchor quantifies one constant C_a before (M, s, ε, θ) and carries the regime γ ≤ C_a^{-1}c⋆^{10} together with the level clause C_a c⋆^{-2}s^{-4}ε^{-2}γ ≤ θ; regime_of_anchor reads the printed regime off that one.

References

• ABK26, p.independence.between.scales; l.good.scales.ratio.lambda; l.ratio.of.good.scales.for.k.

theorem Algsuperdiff.Section4.Provider.Proportion.couplingG0_of_anchor {C Ca cs s ep theta gamma : ℝ} (hC : 6 ≤ C) (hcs0 : 0 < cs) (hcs32 : cs ≤ 3 / 2) (hs0 : 0 < s) (hs12 : s ≤ 1 / 2) (hep0 : 0 < ep) (hep12 : ep ≤ 1 / 2) (hg0 : 0 < gamma) (hCa : C ^ 5 ≤ Ca) (hreg : gamma ≤ Ca⁻¹ * cs ^ 10) (hthetacond : Ca * cs⁻¹ ^ 2 * s⁻¹ ^ 4 * ep⁻¹ ^ 2 * gamma ≤ theta) : C ^ 10 * gamma ^ 2 ≤ theta * cs ^ 8

The 𝒢₀ coupling from the anchor's own clauses. So one C(d) before the parameters costs nothing on this lane.

theorem Algsuperdiff.Section4.Provider.Proportion.couplingG1_of_anchor {K Ca cs s ep theta gamma c1 : ℝ} (hK0 : 0 < K) (hcs0 : 0 < cs) (hcs32 : cs ≤ 3 / 2) (hs0 : 0 < s) (hs12 : s ≤ 1 / 2) (hep0 : 0 < ep) (hg0 : 0 < gamma) (hCa : 3 * K ≤ Ca) (hthetacond : Ca * cs⁻¹ ^ 2 * s⁻¹ ^ 6 * ep⁻¹ ^ 2 * gamma ≤ theta) (hrate : Ca * (c1 * gamma) ≤ cs ^ 2 * s ^ 7 * ep ^ 2 * theta) : K * (1 + c1) * gamma ≤ theta * cs * s ^ 6 * ep ^ 2

The two hypotheses are not the printed ones: the manuscript's e.theta.cond.two and the frozen theorem's clauses carry s^{-4} and s⁵. Nothing downstream consumes the printed condition.

theorem Algsuperdiff.Section4.Provider.Proportion.regime_of_anchor {C Ca cs gamma : ℝ} (hC0 : 0 < C) (hCa : C ^ 10 ≤ Ca) (hreg : gamma ≤ Ca⁻¹ * cs ^ 10) : gamma ≤ C⁻¹ ^ 10 * cs ^ 10

The printed regime is absorbable. The anchor's regime γ ≤ C_a^{-1}c⋆^{10} at any C_a ≥ C^{10} gives the 𝒢₀ lane's printed regime γ ≤ (C^{-1})^{10}c⋆^{10}.