SiteTailCalibrationV2

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

Site-tail calibration at the successor logarithmic exponents

The successor error-moment estimate leads to the Markov exponent

p = c ε² γ⁻¹ |log γ|⁻⁶

and to the accuracy floor K √γ |log γ|^(7/2). Besides the shell and path gates already present in the earlier calibration, the constant K includes 2 e C, which absorbs the additive square-root logarithm in the error-moment amplitude.

This module records the successor constants and the five numerical gates used by the percolation path estimate. It also records the three elementary upper bounds needed when the successor exponent is inserted into the error, regularity, and shell tails.

Successor constants

noncomputable def Algsuperdiff.Section5.Support.siteMarkovExponentV2 {d : ℕ} (M : Section3.ABKModel d) (c ep : ℝ) : ℝ

The Markov exponent at the successor logarithmic scale.

Equations

• Algsuperdiff.Section5.Support.siteMarkovExponentV2 M c ep = c * ep ^ 2 * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)

noncomputable def Algsuperdiff.Section5.Support.siteBadRateSqV2 {d : ℕ} (M : Section3.ABKModel d) (c ep : ℝ) : ℝ

The squared bad-site rate before the separation shift.

Equations

• Algsuperdiff.Section5.Support.siteBadRateSqV2 M c ep = Algsuperdiff.Section5.Support.siteMarkovExponentV2 M c ep / 2

noncomputable def Algsuperdiff.Section5.Support.siteTailRateSqV2 (d : ℕ) (M : Section3.ABKModel d) (c ep : ℝ) : ℝ

The squared bad-site rate after the separation shift.

Equations

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

noncomputable def Algsuperdiff.Section5.Support.siteTailRateV2 (d : ℕ) (M : Section3.ABKModel d) (c ep : ℝ) : ℝ

The bad-site rate after the separation shift.

Equations

• Algsuperdiff.Section5.Support.siteTailRateV2 d M c ep = √(Algsuperdiff.Section5.Support.siteTailRateSqV2 d M c ep)

noncomputable def Algsuperdiff.Section5.Support.siteEpsLowerConstV2 (d : ℕ) (c Cinj Cpath C : ℝ) : ℝ

The constant in the successor lower bound for the accuracy parameter. The last summand is the contribution of the additive square-root logarithm in the error-moment amplitude.

Equations

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

theorem Algsuperdiff.Section5.Support.siteEpsLowerConstV2_pos (d : ℕ) {c Cinj Cpath C : ℝ} (hCinj : 0 < Cinj) (hC : 0 ≤ C) : 0 < siteEpsLowerConstV2 d c Cinj Cpath C

theorem Algsuperdiff.Section5.Support.inv_siteThresholdConst_le_siteEpsLowerConstV2 (d : ℕ) {c Cinj Cpath C : ℝ} (hC : 0 ≤ C) : (siteThresholdConst Cinj)⁻¹ ≤ siteEpsLowerConstV2 d c Cinj Cpath C

theorem Algsuperdiff.Section5.Support.two_exp_mul_le_siteEpsLowerConstV2 (d : ℕ) {c Cinj Cpath C : ℝ} (hCinj : 0 < Cinj) : 2 * Real.exp 1 * C ≤ siteEpsLowerConstV2 d c Cinj Cpath C

theorem Algsuperdiff.Section5.Support.two_exp_mul_sqrt_mul_rpow_le_of_epsLowerV2 {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hCinj : 0 < Cinj) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : 2 * Real.exp 1 * C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep

The third summand of the floor absorbs the additive term in the error-moment amplitude.

Positivity and logarithmic powers

theorem Algsuperdiff.Section5.Support.siteMarkovExponentV2_pos {d : ℕ} (M : Section3.ABKModel d) {c ep : ℝ} (hc : 0 < c) (hep : 0 < ep) : 0 < siteMarkovExponentV2 M c ep

theorem Algsuperdiff.Section5.Support.abs_log_gamma_zpow_neg_six_le_one {d : ℕ} (M : Section3.ABKModel d) : |Real.log M.gamma| ^ (-6) ≤ 1

theorem Algsuperdiff.Section5.Support.abs_log_gamma_zpow_neg_six_le_inv {d : ℕ} (M : Section3.ABKModel d) : |Real.log M.gamma| ^ (-6) ≤ |Real.log M.gamma|⁻¹

theorem Algsuperdiff.Section5.Support.pos_of_epsLowerV2 {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hCinj : 0 < Cinj) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : 0 < ep

The core lower bound

theorem Algsuperdiff.Section5.Support.le_siteMarkovExponentV2_of_epsLower {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hc : 0 < c) (hCinj : 0 < Cinj) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : 2 * (1 + Real.log 3 + (16 * Cpath) ^ 2) * 3 ^ (sitePathExponent * ↑(Section3.Provider.Percolation.sepShift d)) ≤ siteMarkovExponentV2 M c ep

The successor accuracy floor forces the Markov exponent above the common path-bound gate.

The five path-bound gates

theorem Algsuperdiff.Section5.Support.one_le_siteMarkovExponentV2_of_epsLower {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hc : 0 < c) (hCinj : 0 < Cinj) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : 1 ≤ siteMarkovExponentV2 M c ep

theorem Algsuperdiff.Section5.Support.log_three_le_siteBadRateSqV2_of_epsLower {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hc : 0 < c) (hCinj : 0 < Cinj) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : Real.log 3 ≤ siteBadRateSqV2 M c ep

theorem Algsuperdiff.Section5.Support.one_le_siteThresholdConst_mul_of_epsLowerV2 {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hCinj : 0 < Cinj) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : 1 ≤ siteThresholdConst Cinj * ep * (√M.gamma)⁻¹

theorem Algsuperdiff.Section5.Support.gateBracket_le_siteTailRateSqV2_of_epsLower {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hc : 0 < c) (hCinj : 0 < Cinj) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : 1 + Real.log 3 + (16 * Cpath) ^ 2 ≤ siteTailRateSqV2 d M c ep

theorem Algsuperdiff.Section5.Support.one_le_siteTailRateV2_of_epsLower {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hc : 0 < c) (hCinj : 0 < Cinj) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : 1 ≤ siteTailRateV2 d M c ep

theorem Algsuperdiff.Section5.Support.pathBoundGate_le_siteTailRateV2_of_epsLower {d : ℕ} (M : Section3.ABKModel d) {c Cinj Cpath C ep : ℝ} (hc : 0 < c) (hCinj : 0 < Cinj) (hCpath : 0 ≤ Cpath) (hC : 0 ≤ C) (hlow : siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) : Cpath * (1 / 4)⁻¹ * (sitePathExponent - 1)⁻¹ ≤ siteTailRateV2 d M c ep

Upper gates for the three tail estimates

theorem Algsuperdiff.Section5.Support.siteMarkovExponentV2_le_range {d : ℕ} (M : Section3.ABKModel d) {c Crange ep : ℝ} (hCrange : 0 < Crange) (hc : c ≤ Crange⁻¹) (hep : 0 < ep) (hep4 : ep ≤ 1 / 4) : siteMarkovExponentV2 M c ep ≤ Crange⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹

theorem Algsuperdiff.Section5.Support.siteMarkovExponentV2_le_regularity {d : ℕ} (M : Section3.ABKModel d) {c creg ep : ℝ} (hc : c ≤ creg) (hcreg : 0 ≤ creg) (hep : 0 < ep) (hep4 : ep ≤ 1 / 4) : siteMarkovExponentV2 M c ep ≤ creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) * Real.log 2

theorem Algsuperdiff.Section5.Support.siteMarkovExponentV2_le_shell {d : ℕ} (M : Section3.ABKModel d) {c Cinj ep : ℝ} (hc : c ≤ siteThresholdConst Cinj ^ 2) : siteMarkovExponentV2 M c ep ≤ siteThresholdConst Cinj ^ 2 * ep ^ 2 * M.gamma⁻¹