HomStepOneArith

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

Theorem B, §4.5, Step 1: the γ-smallness web of the parameter

selection

This module contains ONLY the elementary real arithmetic that discharges the binders of the anchor Algsuperdiff.Frozen.Section4.bounds_mathcal_E_aL at the §4.5 parameter selection s = |log γ|⁻¹, k = ⌈10|log γ|⌉, n = m - k. It is kept separate from the anchor-consumption module so that the consumption itself reads as the source's own four-line instantiation.

Everything is stated in the γ-quartic-root gauge t:= √(√γ) (so γ = t⁴), which is the smallest gauge in which BOTH the source's |log γ| √γ → 0 and its |log γ| ≤ γ⁻¹ demands are elementary. The correction is honoured: every γ-dependence stays visible and no |log γ|-power is absorbed into a constant.

1. The quartic-root gauge

theorem Algsuperdiff.Section4.Provider.Homogenization.quarticRoot_pow_four {gamma : ℝ} (h : 0 ≤ gamma) : √√gamma ^ 4 = gamma

t:= √(√γ), the quartic root: t⁴ = γ.

theorem Algsuperdiff.Section4.Provider.Homogenization.quarticRoot_pos {gamma : ℝ} (h : 0 < gamma) : 0 < √√gamma

theorem Algsuperdiff.Section4.Provider.Homogenization.quarticRoot_sq (gamma : ℝ) : √√gamma ^ 2 = √gamma

theorem Algsuperdiff.Section4.Provider.Homogenization.quarticRoot_le {gamma b : ℝ} (hg : 0 ≤ gamma) (hb : 0 ≤ b) (h : gamma ≤ b ^ 4) : √√gamma ≤ b

The gauge transfer: γ ≤ b⁴ with b ≥ 0 is t ≤ b.

2. |log γ| in the quartic gauge

theorem Algsuperdiff.Section4.Provider.Homogenization.absLog_le_four_div_quarticRoot {gamma : ℝ} (hg : 0 < gamma) (hg1 : gamma < 1) : |Real.log gamma| ≤ 4 * (√√gamma)⁻¹

|log γ| ≤ 4 t⁻¹ for 0 < γ < 1: the elementary bound log x ≤ x - 1 applied to t⁻¹. This is the only place a logarithm is compared with a power of γ.

theorem Algsuperdiff.Section4.Provider.Homogenization.absLog_mul_sqrt_le {gamma : ℝ} (hg : 0 < gamma) (hg1 : gamma < 1) : |Real.log gamma| * √gamma ≤ 4 * √√gamma

|log γ| √γ ≤ 4 t: the vanishing that the anchor's lower s-endpoint C² √γ ≤ s needs.

3. The two smallness gates in explicit numeric form

theorem Algsuperdiff.Section4.Provider.Homogenization.exp_four_le : Real.exp 4 ≤ 81

exp 4 ≤ 81: the crude form of e ≤ 3, all that the |log γ| ≥ 4 gate needs.

theorem Algsuperdiff.Section4.Provider.Homogenization.four_le_absLog {gamma : ℝ} (hg : 0 < gamma) (hsmall : gamma ≤ 1 / 81) : 4 ≤ |Real.log gamma|

The gate in numeric form: γ ≤ 1/81 forces 4 ≤ |log γ|, hence s = |log γ|⁻¹ ≤ 1/4.

4. The §4.5 parameter facts under the two gates

theorem Algsuperdiff.Section4.Provider.Homogenization.homS_pos_of_four {d : ℕ} (M : Section3.ABKModel d) (h : 4 ≤ |Real.log M.gamma|) : 0 < homS M

s = |log γ|⁻¹ is positive under the |log γ| ≥ 4 gate.

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_homK_le {d : ℕ} (M : Section3.ABKModel d) (h : 4 ≤ |Real.log M.gamma|) : √↑(homK M) ≤ 2 * |Real.log M.gamma|

√k ≤ 2|log γ| under the |log γ| ≥ 4 gate.

theorem Algsuperdiff.Section4.Provider.Homogenization.homK_le_inv_gamma {d : ℕ} (M : Section3.ABKModel d) (hg : 0 < M.gamma) (hg1 : M.gamma < 1) (ht : √√M.gamma ≤ 1 / 16) : ↑(homK M) ≤ M.gamma⁻¹

The mesoscale-gap binder m ≤ n + γ⁻¹ of the anchor, in the form k ≤ γ⁻¹, under t ≤ 1/16.