StepFiveShomComparison

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

t.regularity Step 5: the σ scale comparison

The gap, and how it is closed

ABK26 t.regularity Step 5, asserts inline and WITHOUT citation

   3^{j/2} σ_j^{-1}  ≤  C 3^{-(1/2 - γ)(m-j)} · 3^{m/2} σ_m^{-1} .

Multiplying through by σ_j σ_m 3^{-m/2} > 0, this is exactly the growth cap

   σ_m  ≤  C 3^{γ(m-j)} σ_j                     (j ≤ m) .

The paper never states that cap. l.shom.continuity prints only the mirror direction σ_m ≥ (1/4) σ_n, whose proof reads e.shom.h.bounds in one direction:

   (1/4) max{c⋆γ^{-1}3^{2γm}, ν²}  ≤  σ_m²  ≤  4 max{c⋆γ^{-1}3^{2γm}, ν²} .

The growth cap is the SAME three-line argument read in the other direction, replacing the monotonicity of m ↦ max{c⋆γ^{-1}3^{2γm}, ν²} by its exact geometric growth. That growth is proved as Algsuperdiff.Section3.Provider.Diffusivity.ShomContinuityCore.diffMax_le_rpow_mul, so the cap follows from e.shom.h.bounds alone — i.e. from conjunct 1 of the frozen Algsuperdiff.Frozen.Section3.inductionState, with C = 4 explicit and NO further regime gate (in particular no mStarStar gate, no E-budget and no γ ≤ E^{-10}).

References

• ABK26, t.regularity Step 5, (the uncited comparison).
• ABK26, e.shom.h.bounds; l.shom.continuity.

1. Abstract-real atoms

Every step whose goal would contain Real.rpow is factored through one of these, so no arithmetic tactic ever meets a transcendental atom.

theorem Algsuperdiff.Section4.Provider.Regularity.le_four_mul_of_sq_le {sm sn t Dm Dn : ℝ} (hsm : 0 ≤ sm) (hsn : 0 < sn) (ht : 1 ≤ t) (hup : sm ^ 2 ≤ 4 * Dm) (hcomp : Dm ≤ t * t * Dn) (hlo : 1 / 4 * Dn ≤ sn ^ 2) : sm ≤ 4 * t * sn

The square-comparison core of the growth cap: from s_m² ≤ 4 D_m, D_m ≤ t² D_n and (1/4) D_n ≤ s_n² with t ≥ 1, one gets s_m ≤ 4 t s_n. Abstract reals only.

theorem Algsuperdiff.Section4.Provider.Regularity.inv_le_mul_inv_of_le_mul {a b K : ℝ} (ha : 0 < a) (hb : 0 < b) (h : b ≤ K * a) : a⁻¹ ≤ K * b⁻¹

Inverting a one-sided comparison of positive reals: b ≤ K a gives a⁻¹ ≤ K b⁻¹. Abstract reals only.

theorem Algsuperdiff.Section4.Provider.Regularity.weighted_comparison_aux {A T R S x y : ℝ} (hA : 0 ≤ A) (hid : A * T = R * S) (hxy : x ≤ 4 * T * y) : A * x ≤ 4 * R * (S * y)

Reweighting a comparison by a nonnegative factor, with the transcendental identity supplied as hid: A T = R S. Abstract reals only.

2. The rpow/zpow bridge

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_mul_intCast (a : ℝ) (k : ℤ) : 3 ^ (a * ↑k) = (3 ^ a) ^ k

3^{a k} = (3^a)^k for an integer k: the bridge that turns the source's real-exponent comparison into the integer-exponent geometric ratio that StepFiveGeometricTail sums.

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_neg_half_add_gamma_pos (gamma : ℝ) : 0 < 3 ^ (-(1 / 2 - gamma))

The Step-5 geometric ratio r₁ := 3^{-(1/2 - γ)} is positive.

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_neg_half_add_gamma_lt_one {gamma : ℝ} (hgamma : gamma < 1 / 2) : 3 ^ (-(1 / 2 - gamma)) < 1

The Step-5 geometric ratio r₁ := 3^{-(1/2 - γ)} is < 1 exactly because γ < 1/2, which the shell-law prefix guarantees (γ ≤ 1/4).

3. The growth cap σ_m ≤ 4 · 3^{γ(m-j)} σ_j

theorem Algsuperdiff.Section4.Provider.Regularity.sigmaBar_le_rpow_mul_sigmaBar_of_inductionState {d : ℕ} {M : Section3.ABKModel d} {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {j m : ℤ} (hjm : j ≤ m) (hm : m ≤ m0) : ↑(Section3.Annealed.sigmaBar M m) ≤ 4 * 3 ^ (M.gamma * (↑m - ↑j)) * ↑(Section3.Annealed.sigmaBar M j)

   σ_m  ≤  4 · 3^{γ(m-j)} · σ_j          for  j ≤ m ≤ m₀ .

4. The scale comparison in the weighted form Step 5 consumes

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_half_mul_inv_sigmaBar_le_of_inductionState {d : ℕ} {M : Section3.ABKModel d} {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {j m : ℤ} (hjm : j ≤ m) (hm : m ≤ m0) : 3 ^ (↑j / 2) * (↑(Section3.Annealed.sigmaBar M j))⁻¹ ≤ 4 * (3 ^ (-(1 / 2 - M.gamma))) ^ (m - j) * (3 ^ (↑m / 2) * (↑(Section3.Annealed.sigmaBar M m))⁻¹)

The Step-5 scale comparison, at the explicit constant 4 and with the (m-j)-power written as an integer power of the fixed ratio r₁ = 3^{-(1/2-γ)} ∈ (0,1), which is the shape StepFiveGeometricTail sums:

   3^{j/2} σ_j^{-1}  ≤  4 · r₁^{m-j} · ( 3^{m/2} σ_m^{-1} )      (j ≤ m ≤ m₀) .