G2RatioTail

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

The two per-cube amplitudes of the 𝒢₂ lane

ABK26, §4.1, l.ratio.of.good.scales.for.mathcal.E composed into e.no.bad.scales.applied.for.lambdas for the 𝒢₂ lane.

• cubeAmpOne — the Γ_2-lane per-cube amplitude produced by the Section 3 anchor through G2CubeBound: √3·(1+2d log 3)^{1/2}·C c⋆^{−1}s^{−1}√γ;
• cubeAmpTwo — the Γ_{1/2}-lane per-cube amplitude of the same anchor: √3·(1+2d log 3)²·exp(−C^{−1}c⋆³γ^{−1}).

Scope

Provider material: proved local helpers. The c⋆^{10} regime is carried explicitly, exactly as the anchor states it.

References

• ABK26, l.ratio.of.good.scales.for.mathcal.E.

1. The two per-cube amplitudes of the anchor

noncomputable def Algsuperdiff.Section4.Provider.Proportion.cubeAmpOne (d : ℕ) (C : ℝ) (M : Section3.ABKModel d) (s : ℝ) : ℝ

The Γ_2-lane per-cube amplitude produced by the Section 3 anchor through G2CubeBound: √3·(1+2d log 3)^{1/2}·C c⋆^{−1}s^{−1}√γ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section4.Provider.Proportion.cubeAmpTwo (d : ℕ) (C : ℝ) (M : Section3.ABKModel d) : ℝ

The Γ_{1/2}-lane per-cube amplitude produced by the Section 3 anchor through G2CubeBound: √3·(1+2d log 3)²·exp(−C^{−1}c⋆³γ^{−1}).

Equations

• One or more equations did not get rendered due to their size.