ProfileConstants

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

Parameter arithmetic for the coarse-ellipticity profiles

This file isolates the part of the constant selection for ABK26 p.cg.ellipticity.bounds that follows from the exact frozen gates. It fixes the manuscript's Step-3 parameter b = 2^{-20}, makes the outer sigma ↦ sigma / 4 substitution explicit, and proves that a dimension-only threshold supplies:

• the exponential and b^{-1} gates of e.hsep.tails;
• the four raw localization/oscillation gates used by the bad-cluster proof;
• the smallness of gamma / b needed to retain the frozen Orlicz exponent; and
• the large-rate absorption of a dimension-only prefactor into the frozen rare exponential.

Frozen maximum versus the preliminary package

The older hsep interface assumes the stronger preliminary package

badClustersConst d <= E * cstar M.

The frozen hypothesis supplies only cstar M⁻¹ <= E, so those two statements remain non-interchangeable. The declarations in the raw-gate section below do not assert the stronger package. They instead derive exactly what the proof uses: 4 <= E, unitGate M, gamma <= 1/20, E⁻² <= cstar, and gamma <= E⁻⁵. The percolation providers consume those consequences through their _of_gates interfaces. Final selection of Clow, Cup, and Ccg still belongs to the coarse-ellipticity assembly.

References

• ABK26.

The fixed Step-3 parameters

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileB : ℝ

The manuscript's fixed Whitney-slope parameter b = 2^{-20}.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileB = (2 ^ 20)⁻¹

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileSigma (sigma : ℝ) : ℝ

The sigma ↦ sigma / 4 substitution used before the two scale sums.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileSigma sigma = sigma / 4

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileB_pos : 0 < bfaProfileB

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileB_le_one_ninth : bfaProfileB ≤ 1 / 9

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileB_le_one_eighth : bfaProfileB ≤ 1 / 8

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileSigma_pos {sigma : ℝ} (hsigma : 0 < sigma) : 0 < bfaProfileSigma sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileSigma_le_one_eighth {sigma : ℝ} (hsigma : sigma ≤ 1 / 2) : bfaProfileSigma sigma ≤ 1 / 8

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileSigma_le_one_half {sigma : ℝ} (hsigma : sigma ≤ 1 / 2) : bfaProfileSigma sigma ≤ 1 / 2

A dimension-only gate constant

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.profileAuxiliaryConst (d : ℕ) : ℝ

A dimension-only constant sufficient for the hsep exponential gate, the fixed b^{-1} gate, and the Orlicz-index comparison. It deliberately does not encode the unavailable E * cstar gate.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.profileAuxiliaryConst_pos (d : ℕ) : 0 < profileAuxiliaryConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.four_mul_badClustersConst_le_profileAuxiliaryConst (d : ℕ) : 4 * Percolation.badClustersConst d ≤ profileAuxiliaryConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.badClustersConst_div_bfaProfileB_le_profileAuxiliaryConst (d : ℕ) : Percolation.badClustersConst d / bfaProfileB ≤ profileAuxiliaryConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.two_div_fifteen_mul_bfaProfileB_le_profileAuxiliaryConst (d : ℕ) : 2 / (15 * bfaProfileB) ≤ profileAuxiliaryConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exp_badClustersConst_div_bfaProfileSigma_le_of_profileAuxiliaryGate {d : ℕ} {sigma E : ℝ} (hsigma : 0 < sigma) (hgate : Real.exp (profileAuxiliaryConst d / sigma) ≤ E) : Real.exp (Percolation.badClustersConst d / bfaProfileSigma sigma) ≤ E

The frozen exponential gate at sigma supplies the hsep gate at the auxiliary index sigma / 4.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.badClustersConst_div_bfaProfileB_le_of_profileAuxiliaryGate {d : ℕ} {sigma E : ℝ} (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hgate : Real.exp (profileAuxiliaryConst d / sigma) ≤ E) : Percolation.badClustersConst d / bfaProfileB ≤ E

The same frozen exponential gate pays the fixed b^{-1} threshold.

The raw bad-event gates from the frozen maximum

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.four_le_of_profileAuxiliaryMaxGate {d : ℕ} {M : ABKModel d} {sigma E : ℝ} (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hgate : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) : 4 ≤ E

The exponential branch of the frozen maximum is already large enough to force the local-probability gate 4 <= E.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.inv_le_cstar_of_profileAuxiliaryMaxGate {d : ℕ} {M : ABKModel d} {sigma E : ℝ} (hE : 1 ≤ E) (hgate : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) : E⁻¹ ≤ Disorder.cstar M

The inverse branch of the frozen maximum, rewritten without inversion.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.inv_sq_le_cstar_of_profileAuxiliaryMaxGate {d : ℕ} {M : ABKModel d} {sigma E : ℝ} (hE : 1 ≤ E) (hgate : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) : E⁻¹ ^ 2 ≤ Disorder.cstar M

The inverse branch also gives the weaker square-inverse gate used by the printed oscillation tail.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.unitGate_of_cstar_mul_gammaInv {d : ℕ} (M : ABKModel d) (hratio : 25 / BadEvents.deltaOsc d ^ 2 ≤ Disorder.cstar M * M.gamma⁻¹) : BadEvents.unitGate M

A lower bound on cstar * gamma⁻¹ opens the threshold of the oscillation weak-Orlicz tail.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.unitGate_of_profileAuxiliaryMaxGate {d : ℕ} (M : ABKModel d) {sigma E : ℝ} (hE : 1 ≤ E) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) : BadEvents.unitGate M

The exact frozen maximum and fifth-root gates imply the oscillation threshold gate, without the stronger preliminary assumption C <= E * cstar.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gamma_le_zpow_neg_five_of_frozenGate {E gamma : ℝ} (hE : 1 ≤ E) (hgamma : 0 < gamma) (hEgamma : E ≤ gamma ^ (-(1 / 5))) : gamma ≤ E ^ (-5)

The frozen fifth-root gate in the integer-power form consumed by the percolation and multiscale providers.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.badEventGates_of_profileAuxiliaryMaxGate {d : ℕ} (M : ABKModel d) {sigma E : ℝ} (hE : 1 ≤ E) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) : 4 ≤ E ∧ BadEvents.unitGate M ∧ M.gamma ≤ 1 / 20 ∧ E⁻¹ ^ 2 ≤ Disorder.cstar M ∧ M.gamma ≤ E ^ (-5)

The four raw probability gates and the integer fifth-power tuning obtained from the exact frozen hypotheses.

The frozen exponent after the sigma / 4 substitution

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.zpow_neg_five_le_three_halves_mul_of_exp_div_le {C b sigma E : ℝ} (hC : 0 < C) (hb : 0 < b) (hsigma : 0 < sigma) (hfloor : 2 / (15 * b) ≤ C) (hgate : Real.exp (C / sigma) ≤ E) : E ^ (-5) ≤ 3 / 2 * b * sigma

The elementary decay estimate used to turn the exponential threshold into gamma / b = O(sigma).

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.zpow_neg_five_le_three_halves_mul_bfaProfileB_of_profileAuxiliaryGate {d : ℕ} {sigma E : ℝ} (hsigma : 0 < sigma) (hgate : Real.exp (profileAuxiliaryConst d / sigma) ≤ E) : E ^ (-5) ≤ 3 / 2 * bfaProfileB * sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.half_one_sub_le_bfaTau_profileSigma {sigma gam b : ℝ} (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hgam : 0 < gam) (hb : 0 < b) (hsmall : gam ≤ 3 / 2 * b * sigma) : (1 - sigma) / 2 ≤ Multiscale.bfaTau (bfaProfileSigma sigma) gam b

If gamma / b is paid by the frozen exponential gate, the internal B lane is at least as strong as the frozen Gamma_{(1-sigma)/2} lane.

Absorbing dimension-only factors at a large rare rate