StepOneParameters

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

t.regularity Step 1: the parameter web (k, s, δ), the C₁-largeness

demands, and the pins

The target

k := ⌈4 log₃ (2 s^{-3/2} C_{e.excess.decay.one.step})⌉ ,   s := 1/4 ,
δ := C₁⁻¹(1 - α) ,                          C₁ = C₁(d, c⋆) large enough.

The excess-decay one-step constant is NOT yet fixed anywhere in the repository, so it is carried here as the abstract real Cedos; every statement below is uniform in it.

Contents

• stepOneKArg, stepOneK — the printed k. The ceiling is Nat.ceil because the source says k ∈ ℕ; at C_edos ≥ 1 the argument of the logarithm exceeds 1, so Nat.ceil and Int.ceil agree there.
• stepOneThreePow, stepOneDelta0, stepOneC1Delta0 — the third Step-1 bullet: the factor 3^{k/4}, the threshold δ₀ defined by δ₀^{1/2} s^{-1/2} C_edos C_ann = ½ 3^{-k/4}, and its C₁-floor δ₀⁻¹.
• stepOneC1 and its four largeness demands.
• stepOneEp — the good-event threshold ⅛ s δ^{1/2}.
• StepOneBadSetSeparation — the pin.

Deviations from the printed text

1. The printed first bullet reads γ|log γ|² ≤ s c⋆² (⅛ s δ^{1/2}) with the Step-1 s = 1/4 in the first slot. The annular producer is applied at the index s/8 (that is the index inside 𝒢(j, z; ⅛s, ⅛ s δ^{1/2}) and inside ε_j(z)), so the honest requirement is at (s/8)^{3/2}; that is the form StepOneEpsilon.lean carries. Both differ from the print by a fixed numerical factor only (s is the numeral 1/4).
2. s^{-3/2} and 3^{-k/4} are written with Real.rpow, as the frozen theorems do. 3^{-k/4} is kept opaque (only positivity and Real.rpow_neg are used), so no transcendental atom ever reaches a numeric tactic.

References

• ABK26, t.regularity Step 1.

1. The s-powers at the Step-1 numeral s = 1/4

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneS_eq : stepOneS = 1 / 4

s = 1/4.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneS_pos : 0 < stepOneS

0 < s.

2. The Step-1 integer k

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneKArg (Cedos : ℝ) : ℝ

The argument of the logarithm in e.parameter.choices.regularity: 2 s^{-3/2} C_{e.excess.decay.one.step}. Cedos is the abstract excess-decay one-step constant.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneKArg Cedos = 2 * Algsuperdiff.Section4.Provider.Regularity.stepOneS.rpow (-(3 / 2)) * Cedos

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneK (Cedos : ℝ) : ℕ

k := ⌈4 log₃ (2 s^{-3/2} C_{e.excess.decay.one.step})⌉ of e.parameter.choices.regularity, as a function of the abstract excess-decay one-step constant.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneK Cedos = ⌈4 * Real.logb 3 (Algsuperdiff.Section4.Provider.Regularity.stepOneKArg Cedos)⌉₊

3. The factor 3^{k/4}

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneThreePow (k : ℕ) : ℝ

3^{k/4}, the factor of the third Step-1 bullet, kept opaque.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneThreePow k = Real.rpow 3 (↑k / 4)

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneThreePow_pos (k : ℕ) : 0 < stepOneThreePow k

0 < 3^{k/4}.

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_three_neg_quarter (k : ℕ) : Real.rpow 3 (-↑k / 4) = (stepOneThreePow k)⁻¹

3^{-k/4} = (3^{k/4})⁻¹.

4. The third Step-1 bullet: δ ≤ δ₀

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneDelta0 (Cedos Cann : ℝ) (k : ℕ) : ℝ

δ₀ of the third Step-1 bullet: the largest tolerance with δ₀^{1/2} s^{-1/2} C_edos C_ann ≤ ½ 3^{-k/4}, here taken with equality.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneC1Delta0 (Cedos Cann : ℝ) (k : ℕ) : ℝ

The C₁-floor of the largeness condition: C₁ ≥ δ₀⁻¹ forces δ = C₁⁻¹(1-α) ≤ δ₀.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneC1Delta0 Cedos Cann k = (Algsuperdiff.Section4.Provider.Regularity.stepOneDelta0 Cedos Cann k)⁻¹

5. The four largeness demands on C₁

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneC1 (d : ℕ) (Cedos Cann Citer : ℝ) (k : ℕ) : ℝ

The Step-1 constant C₁, as the maximum of the largeness demands: the δ-window pin C₁ ≥ 2 of p.minimal.scale.separation.sec4, the Step-7 volume/transport pins C₁ ≥ 2d and C₁ ≥ 2(d + γ) (γ ≤ 1 in the regime), the Step-6 demand C₁ ≥ 4 C_iter (k+1)/log 3, and the δ₀ threshold of the third bullet. Citer is the abstract Step-6 iteration constant, Cann the annular one, Cedos the excess-decay one-step one; all three depend only on d, so C₁ = C₁(d) — inside the printed C₁ = C₁(d, c⋆).

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.two_le_stepOneC1 (d : ℕ) (Cedos Cann Citer : ℝ) (k : ℕ) : 2 ≤ stepOneC1 d Cedos Cann Citer k

pin: C₁ ≥ 2, the pin that puts δ = C₁⁻¹(1-α) inside the (0,1/2] window of p.minimal.scale.separation.sec4.

theorem Algsuperdiff.Section4.Provider.Regularity.two_mul_dim_le_stepOneC1 (d : ℕ) (Cedos Cann Citer : ℝ) (k : ℕ) : 2 * ↑d + 2 ≤ stepOneC1 d Cedos Cann Citer k

pins (3) and (4): C₁ ≥ 2d, and C₁ ≥ 2(d + γ) whenever γ ≤ 1 — the Step-7 volume factor 3^{(d/2)(n'-n)} and the coarse-graining transport 3^{(1/2)(d+γ)(m-m')}.

theorem Algsuperdiff.Section4.Provider.Regularity.step6_le_stepOneC1 (d : ℕ) (Cedos Cann Citer : ℝ) (k : ℕ) : 4 * Citer * (↑k + 1) / Real.log 3 ≤ stepOneC1 d Cedos Cann Citer k

pin (2): C₁ ≥ 4 C_iter (k+1)/log 3, the Step-6 demand.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneC1_pos (d : ℕ) (Cedos Cann Citer : ℝ) (k : ℕ) : 0 < stepOneC1 d Cedos Cann Citer k

0 < C₁.

6. The good-event threshold ⅛ s δ^{1/2}

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneEp (delta : ℝ) : ℝ

The Step-1 good-event threshold ⅛ s δ^{1/2}, which is also the threshold s' √δ of p.minimal.scale.separation.sec4 at the Step-1 slot s' = s/8.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneEp delta = Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth * √delta

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneEp_mem_Ioc {delta : ℝ} (hdelta : delta ∈ Set.Ioc 0 (1 / 2)) : stepOneEp delta ∈ Set.Ioc 0 (1 / 2)

⅛ s δ^{1/2} ∈ (0, 1/2]: the ε-range of the annular producer's clause (ii).

9. The pins

def Algsuperdiff.Section4.Provider.Regularity.StepOneBadSetSeparation (badCard : ℕ) (n m : ℤ) : Prop

The separation side condition, recorded as a named demand for the windows and bad-set step: the number of bad scales in the window plus 7 must not exceed the window length. It resolves the n' = m' reading by supplying exactly this condition; it is a presentational gap in the manuscript, NOT discharged here — the bad set is not formed in this module.

Equations

• Algsuperdiff.Section4.Provider.Regularity.StepOneBadSetSeparation badCard n m = (↑badCard + 7 ≤ m - n)

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneBadSetSeparation_of_le {badCard : ℕ} {n m : ℤ} (h : badCard + 7 ≤ (m - n).toNat) : StepOneBadSetSeparation badCard n m

The separation demand in the ℕ-form a bad-set cardinality bound produces.