RootClauseBCloseArith

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

1. The interior window's volume at an arbitrary scale

theorem Algsuperdiff.Section4.Provider.Regularity.three_zpow_pow_eq_rpow (a : ℤ) (e : ℕ) : (3 ^ a) ^ e = Real.rpow 3 (↑a * ↑e)

(3^a)^{d} as a real power of 3.

theorem Algsuperdiff.Section4.Provider.Regularity.volume_toReal_truncatedWindow_inner_gen (d : ℕ) {m j : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1))) (hj : j ≤ m - 1) : (MeasureTheory.volume (ExcessDecay.truncatedWindow z m j)).toReal = (3 ^ j) ^ d

On the interior branch the window (z+□_j) ∩ □_m IS the translate z + □_j for every j ≤ m-1, so its volume is exactly 3^{dj}.

theorem Algsuperdiff.Section4.Provider.Regularity.volumeRatio_inner_gen (d : ℕ) (m j : ℤ) : (3 ^ m) ^ d / (3 ^ j) ^ d = (3 ^ (m - j)) ^ d

The volume ratio of the interior window at scale j inside □_m.

2. The window-to-cube step of hgradE, at an arbitrary interior scale

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenNuGradNorm_window_le_cube (d : ℕ) {m j : ℤ} {z : HCPolySupport.Vec d} {nu : ℝ} (hnu : 0 ≤ nu) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1))) (hj : j ≤ m - 1) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : stepSevenNuGradNorm nu (ExcessDecay.truncatedWindow z m j) u.grad ≤ √((3 ^ (m - j)) ^ d) * stepSevenNuGradNorm nu (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.grad

The K_g slot of the chain, at a general coarse scale.

  ν^{1/2}‖∇u‖_{L²((z+□_j) ∩ □_m)}  ≤  3^{(m-j)d/2} · ν^{1/2}‖∇u‖_{L²(□_m)} .

The case j = m-1 is the one the close chain consumes. Not an estimate on u: integral monotonicity on nested sets plus the exact volume computation of §1.

3. The three re-cut constants

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopKg (d : ℕ) (m k : ℤ) : ℝ

The K_g slot at the chain's coarse scale k: the exact volume ratio 3^{(m-k)d/2}.

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopKg d m k = √((3 ^ (m - k)) ^ d)

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopKg_eq (d : ℕ) (m k : ℤ) : rootClauseBTopKg d m k = Real.rpow 3 ((↑m - ↑k) * ↑d / 2)

K_g in exponential form.

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopKs (gamma : ℝ) (m ks : ℤ) : ℝ

The K_s slot: the σ index gap 4·3^{γ(m-k⋆)} between the coarse record's own σ_{k⋆} and the display's σ_m.

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopKs gamma m ks = 4 * Real.rpow 3 (gamma * (↑m - ↑ks))

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopKs_nonneg (gamma : ℝ) (m ks : ℤ) : 0 ≤ rootClauseBTopKs gamma m ks

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopCtr (d : ℕ) (Kd : ℝ) : ℝ

The C_tr slot of the re-cut: max(2·3^{d+1/2}, 4·3^{3/4}K_d). A pure (d, K_d) constant — no sample, no scale, no α, no γ.

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopCtr d Kd = max (2 * Real.rpow 3 (↑d + 1 / 2)) (4 * Real.rpow 3 (3 / 4) * Kd)

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBTopCtr_nonneg (d : ℕ) (Kd : ℝ) : 0 ≤ rootClauseBTopCtr d Kd

4. The δ-linear exponent budget

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBExpBudget {dd c alpha delta C1 T Bb G : ℝ} (hdd : 0 ≤ dd) (hc0 : 0 ≤ c) (hcC1 : 4 * c ≤ 2 * dd + 2) (hC1 : 2 * dd + 2 ≤ C1) (halpha0 : 0 ≤ alpha) (halpha1 : alpha ≤ 1) (hdelta : delta ≤ C1⁻¹ * (1 - alpha)) (hT0 : 0 ≤ T) (hbud : Bb ≤ delta * (T + 1)) (hGB : G ≤ Bb + 1) : c * G ≤ 1 / 4 * ((1 - alpha) * T) + (1 / 4 + c)

The gap absorbs.

For any coefficient c ≥ 0 with 4c ≤ 2d+2 (both 1/4 + d/2 and 1/2 qualify), the Step-7c scalar budget forces

  c·G  ≤  (1/4)·(1-α)T  +  (1/4 + c)          whenever  G ≤ |𝓑| + 1 .

The remainder 1/4 + c is free of m, n, α, δ and the sample: this is the whole content of the print's absorption of the bad-scale count into the display's exponent.

5. The two K_tr dominations at the re-cut

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBTop_hKgb (d : ℕ) {gamma alpha delta C1 Kd : ℝ} {n m k : ℤ} {Bb : ℕ} (hgamma : gamma < 1 / 2) (hC1 : 2 * ↑d + 2 ≤ C1) (halpha0 : 0 ≤ alpha) (halpha1 : alpha ≤ 1) (hnm : n ≤ m) (hdelta : delta ≤ C1⁻¹ * (1 - alpha)) (hbud : ↑Bb ≤ delta * (↑(m - n).toNat + 1)) (hks : k + 1 ≤ m) (hgap : m - (k + 1) ≤ ↑Bb + 1) : √(rootClauseBTopKs gamma m (k + 1)) * rootClauseBTopKg d m k ≤ rootClauseBTopCtr d Kd * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m)

The hKgb slot at the re-cut coarse scale.

√K_s·K_g = 2·3^{d/2}·3^{(γ/2 + d/2)(m-k⋆)} and §4 at c = 1/4 + d/2 puts the exponent under d + 1/2 + (1/4)(1-α)(m-n).

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBTop_hKdb (d : ℕ) {gamma alpha delta C1 Kd : ℝ} {n m k : ℤ} {Bb : ℕ} (hgamma : gamma < 1 / 2) (hKd : 0 ≤ Kd) (hC1 : 2 * ↑d + 2 ≤ C1) (halpha0 : 0 ≤ alpha) (halpha1 : alpha ≤ 1) (hnm : n ≤ m) (hdelta : delta ≤ C1⁻¹ * (1 - alpha)) (hbud : ↑Bb ≤ delta * (↑(m - n).toNat + 1)) (hks : k + 1 ≤ m) (hgap : m - (k + 1) ≤ ↑Bb + 1) : rootClauseBTopKs gamma m (k + 1) * Kd ≤ rootClauseBTopCtr d Kd * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m)

The hKdb slot at the re-cut coarse scale.

K_s·K_d = 4·3^{γ(m-k⋆)}·K_d and §4 at c = 1/2 puts the exponent under `3/4

• (1/4)(1-α)(m-n)`.

6. The htrShom slot: the σ index gap, inverted

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBTop_htrShom {d : ℕ} {M : Section3.ABKModel d} {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {ks m : ℤ} (hks : ks ≤ m) (hm : m ≤ m0) : (↑(Section3.Annealed.sigmaBar M ks))⁻¹ ≤ rootClauseBTopKs M.gamma m ks * (↑(Section3.Annealed.sigmaBar M m))⁻¹

The htrShom slot at the re-cut coarse scale.

The proved growth cap σ_m ≤ 4·3^{γ(m-k⋆)}σ_{k⋆} inverted:

  σ_{k⋆}^{-1}  ≤  K_s · σ_m^{-1} ,      K_s = 4·3^{γ(m-k⋆)} .

's K_s = 1 is the case k⋆ = m, where the cap is vacuous.