EarlyExitPrinted

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

The printed early-exit exponent

This file prices the integer subtraction and division in the canonical chain length, and combines that discrete estimate with the auxiliary-scale comparison into the printed bound on the early-exit exponent.

def Algsuperdiff.Section5.Provider.earlyExitBaseScale (d : ℕ) : ℕ

The explicit size threshold which absorbs both endpoint losses and the integer division by the overlap multiplicity.

Equations

• Algsuperdiff.Section5.Provider.earlyExitBaseScale d = 64 * (d + 1 + 3 ^ d)

noncomputable def Algsuperdiff.Section5.Provider.earlyExitDecayConstant (d : ℕ) (gamma delta kappa : ℝ) : ℝ

The explicit coefficient left after the two factor-two losses and the factor three in the auxiliary-scale comparison.

Equations

• Algsuperdiff.Section5.Provider.earlyExitDecayConstant d gamma delta kappa = kappa * delta ^ (1 - gamma)⁻¹ / (192 * 3 ^ d)

theorem Algsuperdiff.Section5.Provider.div_sixteen_pow_le_earlyExitChainLength (d k : ℕ) (hlarge : 64 * (d + 1) ≤ 3 ^ k) : 3 ^ k / (16 * 3 ^ d) ≤ earlyExitChainLength d k

Before taking real casts, the canonical chain contains the quotient by 16 * 3^d; the constant 64 in earlyExitBaseScale pays for the endpoint subtractions.

theorem Algsuperdiff.Section5.Provider.earlyExitChainLength_lower (d k : ℕ) (hlarge : earlyExitBaseScale d ≤ 3 ^ k) : 3 ^ k / (32 * 3 ^ d) ≤ ↑(earlyExitChainLength d k)

In real form, after one further factor two for the final quotient remainder, the canonical chain has length at least 3^k / (32 * 3^d).

theorem Algsuperdiff.Section5.Provider.displacementMinScale_lt_three_mul_displacementScale {nu cstar gamma delta t : ℝ} {m n : ℤ} (hnu : 0 < nu) (ht : 0 < t) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma1 : gamma < 1) (hnm : n ≤ m) (hn : 3 ^ n ≤ Support.auxiliaryScaleBound nu cstar gamma delta t m) : Support.displacementMinScale nu cstar gamma t m < 3 * Support.displacementScale delta gamma (m - n).toNat

The lower half of the auxiliary-scale straddle bounds the printed minimum by the next displacement scale. The factor three is the single successor scale loss.

noncomputable def Algsuperdiff.Section5.Provider.earlyExitProfileCost (cstar gamma : ℝ) : ℝ

The explicit cost of comparing the two terms of the effective diffusivity with the two terms in auxiliaryScaleBound.

Equations

• Algsuperdiff.Section5.Provider.earlyExitProfileCost cstar gamma = 3 + 3 * √(cstar * gamma⁻¹) ^ gamma

theorem Algsuperdiff.Section5.Provider.time_div_lengthTimeScale_le_of_auxiliaryScale_lt {nu cstar gamma delta t : ℝ} {m n : ℤ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma1 : gamma < 1) (hdelta : 0 < delta) (ht : 0 < t) (hnm : n ≤ m) (hn : Support.auxiliaryScaleBound nu cstar gamma delta t m < 3 ^ (n + 1)) : t / Support.lengthTimeScale nu cstar gamma (3 ^ n) ≤ delta * earlyExitProfileCost cstar gamma * 3 ^ (m - n).toNat

The upper half of the auxiliary-scale straddle controls the positive Laplace cost at the profile time scale.

theorem Algsuperdiff.Section5.Provider.laplaceCost_le_of_auxiliaryScale_lt {d : ℕ} (M : Section3.ABKModel d) {cstar C delta t kappa : ℝ} {m n : ℤ} (hcstar : 0 < cstar) (hC : 0 < C) (hdelta : 0 < delta) (ht : 0 < t) (hnm : n ≤ m) (hn : Support.auxiliaryScaleBound M.nu cstar M.gamma delta t m < 3 ^ (n + 1)) (hscale : Support.lengthTimeScale M.nu cstar M.gamma (3 ^ n) ≤ 2 * Support.exitTimeScale M n) (hdeltaSmall : 128 * 3 ^ d * delta * earlyExitProfileCost cstar M.gamma ≤ C * kappa) : (C * Support.exitTimeScale M n)⁻¹ * t ≤ kappa * 3 ^ (m - n).toNat / (64 * 3 ^ d)

The scale straddle and the comparison between the profile time and the running exit-time scale put the positive Laplace term below half of the retained chain exponent.

theorem Algsuperdiff.Section5.Provider.earlyExit_exponent_le {d : ℕ} {nu cstar gamma delta t lam kappa : ℝ} {m n : ℤ} (hnu : 0 < nu) (ht : 0 < t) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma1 : gamma < 1) (hkappa : 0 < kappa) (hnm : n ≤ m) (hn : 3 ^ n ≤ Support.auxiliaryScaleBound nu cstar gamma delta t m) (hlarge : earlyExitBaseScale d ≤ 3 ^ (m - n).toNat) (htime : lam * t ≤ kappa * 3 ^ (m - n).toNat / (64 * 3 ^ d)) : 0 < earlyExitDecayConstant d gamma delta kappa ∧ lam * t - kappa * ↑(earlyExitChainLength d (m - n).toNat) ≤ -earlyExitDecayConstant d gamma delta kappa * Support.displacementMinScale nu cstar gamma t m

Deterministic B8 exponent lemma. The natural-number endpoint and division losses are included in earlyExitChainLength_lower; the successor loss in the auxiliary scale is included in displacementMinScale_lt_three_mul_displacementScale. Once the positive Laplace cost uses at most half of the retained chain exponent, the printed minimum remains with the explicit positive coefficient earlyExitDecayConstant.

noncomputable def Algsuperdiff.Section5.Provider.earlyExitKappa (Cup clow : NNReal) : ℝ

The positive exponent extracted from the strict one-step Laplace contraction.

Equations

• Algsuperdiff.Section5.Provider.earlyExitKappa Cup clow = 1 - (Algsuperdiff.Section5.Provider.oneStepLaplaceContraction Cup clow).toReal

theorem Algsuperdiff.Section5.Provider.earlyExitKappa_pos {Cup clow : NNReal} (hCup : 0 < Cup) (hclow : 0 < clow) : 0 < earlyExitKappa Cup clow

The exponent extracted from the one-step contraction is strictly positive.

theorem Algsuperdiff.Section5.Provider.oneStepLaplaceContraction_le_exp_neg_earlyExitKappa (Cup clow : NNReal) : oneStepLaplaceContraction Cup clow ≤ ENNReal.ofReal (Real.exp (-earlyExitKappa Cup clow))

The strict one-step contraction is bounded by the real exponential of its extracted positive exponent.

theorem Algsuperdiff.Section5.Provider.earlyExit_exponent_le_of_auxiliaryScale_straddle {d : ℕ} (M : Section3.ABKModel d) {C delta t kappa : ℝ} {m n : ℤ} (hC : 0 < C) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (ht : 0 < t) (hkappa : 0 < kappa) (hnm : n ≤ m) (hnLower : 3 ^ n ≤ Support.auxiliaryScaleBound M.nu (Section3.Disorder.cstar M) M.gamma delta t m) (hnUpper : Support.auxiliaryScaleBound M.nu (Section3.Disorder.cstar M) M.gamma delta t m < 3 ^ (n + 1)) (hscale : Support.lengthTimeScale M.nu (Section3.Disorder.cstar M) M.gamma (3 ^ n) ≤ 2 * Support.exitTimeScale M n) (hdeltaSmall : 128 * 3 ^ d * delta * earlyExitProfileCost (Section3.Disorder.cstar M) M.gamma ≤ C * kappa) (hlarge : earlyExitBaseScale d ≤ 3 ^ (m - n).toNat) : 0 < earlyExitDecayConstant d M.gamma delta kappa ∧ (C * Support.exitTimeScale M n)⁻¹ * t - kappa * ↑(earlyExitChainLength d (m - n).toNat) ≤ -earlyExitDecayConstant d M.gamma delta kappa * Support.displacementMinScale M.nu (Section3.Disorder.cstar M) M.gamma t m

Deterministic B8 scale optimization. If n straddles the auxiliary scale, the profile time is comparable to the running exit-time scale, the accuracy is below the displayed explicit threshold, and the residual triadic gap is above earlyExitBaseScale, then the Chernoff exponent is a negative multiple of the exact minimum printed in the paper.