RootClauseBFinalArith

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

1. The M-uniform dataOsc weight

theorem Algsuperdiff.Section4.Provider.Regularity.one_sub_rpow_three_neg_quarter_pos : 0 < 1 - 3 ^ (-(1 / 4))

3^{-1/4} < 1, so the uniform denominator is positive.

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioG_le_rpow_neg_quarter {d : ℕ} {M : Section3.ABKModel d} (hgamma : M.gamma ≤ 1 / 4) : stepFiveRatioG M ≤ 3 ^ (-(1 / 4))

The γ-gated cap on the Step-5 geometric ratio. r₁ = 3^{-(1/2-γ)} is increasing in γ, so the regime clause γ ≤ 1/4 — which the Step-6 producer's own γ ≤ 1/256 implies — pins it below 3^{-1/4}.

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBOscWUniform (Cdel : ℝ) : ℝ

The M-free dataOsc weight 4C_δ/(1-3^{-1/4}).

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBOscWUniform Cdel = 4 * Cdel / (1 - 3 ^ (-(1 / 4)))

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBOscWUniform_nonneg {Cdel : ℝ} (hC : 0 ≤ Cdel) : 0 ≤ rootClauseBOscWUniform Cdel

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalDataOscW_le_uniform {d : ℕ} {M : Section3.ABKModel d} {Cdel : ℝ} (hgamma : M.gamma < 1 / 2) (hquarter : M.gamma ≤ 1 / 4) (hC : 0 ≤ Cdel) : edFinalDataOscW M Cdel ≤ rootClauseBOscWUniform Cdel

The M-uniform funding enlargement. Inside the regime γ ≤ 1/4 the dataOsc weight is bounded by a constant free of the model.

2. The α-uniform A6 cap constant

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepOneEpUniform : ℝ

The α-free Step-1 amplitude ε₀ = (s/8)·√(1/2), the value of stepOneEp at the top of the Step-1 window δ ≤ 1/2.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepOneEpUniform = Algsuperdiff.Section4.Provider.Regularity.stepOneSEighth * √(1 / 2)

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneEp_le_stepOneEpUniform {delta : ℝ} (hdelta : delta ≤ 1 / 2) : stepOneEp delta ≤ stepOneEpUniform

, the amplitude half: ε(δ) = (s/8)√δ ≤ (s/8)/√2 for every δ in the Step-1 window.

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBCapsUniform (d : ℕ) (C : ℝ) : ℝ

The α-free A6 cap constant 2d((C·ε₀)²+1).

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBCapsUniform d C = 2 * ↑d * ((C * Algsuperdiff.Section4.Provider.Regularity.stepOneEpUniform) ^ 2 + 1)

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBCapsUniform_nonneg (d : ℕ) (C : ℝ) : 0 ≤ rootClauseBCapsUniform d C

theorem Algsuperdiff.Section4.Provider.Regularity.capsConst_le_rootClauseBCapsUniform (d : ℕ) {C delta : ℝ} (hC : 0 ≤ C) (hdelta : delta ≤ 1 / 2) : 2 * ↑d * ((C * stepOneEp delta) ^ 2 + 1) ≤ rootClauseBCapsUniform d C

, the cap half: the produced A6 constant 2d((C·ε(δ))²+1) is below its value at the top of the Step-1 window, uniformly in α.

3. The four remaining monotone slots of the composite prefactor

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBCg_mono_cbc (d : ℕ) {Ccacc Cosc CBc CBc' : ℝ} (hCcacc : 0 ≤ Ccacc) (hCosc : 0 ≤ Cosc) (h : CBc ≤ CBc') : rootClauseBCg d Ccacc Cosc CBc ≤ rootClauseBCg d Ccacc Cosc CBc'

rootClauseBCg is monotone in its C_Bc slot.

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBCg_nonneg (d : ℕ) {Ccacc Cosc CBc : ℝ} (hCcacc : 0 ≤ Ccacc) (hCosc : 0 ≤ Cosc) : 0 ≤ rootClauseBCg d Ccacc Cosc CBc

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBPrefactor_mono_data (d : ℕ) {Cch Ccacc Cosc CBc CBc' CB CB' Ctr CWG CWG' CdM CdM' : ℝ} (hCch : 0 ≤ Cch) (hCcacc : 0 ≤ Ccacc) (hCosc : 0 ≤ Cosc) (hCB : 0 ≤ CB) (hCtr : 0 ≤ Ctr) (hCWG : 0 ≤ CWG) (hCdM : 0 ≤ CdM) (hBc : CBc ≤ CBc') (hB : CB ≤ CB') (hWG : CWG ≤ CWG') (hdM : CdM ≤ CdM') : rootClauseBPrefactor d Cch Ccacc Cosc CBc CB Ctr CWG CdM ≤ rootClauseBPrefactor d Cch Ccacc Cosc CBc' CB' Ctr CWG' CdM'

The composite clause-(B) prefactor is monotone in its four data slots.

C_Bc enters only through rootClauseBCg, C_B only through the bracket √(32/7 C_B) + 32/7 C_B, and C_WG, C_dM only additively; all four are monotone at the endpoint's own nonnegativity binders. This is what lets the M-uniform C_WG of §1 and the α-uniform C_B of §2 be substituted into the funding hypothesis.

4. The γ|log γ|² thresholds

theorem Algsuperdiff.Section4.Provider.Regularity.abs_log_le_rpow_neg_eighth {g : ℝ} (hg0 : 0 < g) (hg1 : g ≤ 1) : |Real.log g| ≤ 8 * g ^ (-(1 / 8))

|log γ| ≤ 8 γ^{-1/8} on (0,1], from log x ≤ x - 1 at x = γ^{-1/8}.

theorem Algsuperdiff.Section4.Provider.Regularity.gamma_mul_log_sq_le {g : ℝ} (hg0 : 0 < g) (hg1 : g ≤ 1) : g * |Real.log g| ^ 2 ≤ 64 * g ^ (3 / 4)

The elementary γ|log γ|² bound. For 0 < γ ≤ 1, γ|log γ|² ≤ 64 γ^{3/4}.

theorem Algsuperdiff.Section4.Provider.Regularity.gamma_log_sq_le_of_le_threshold {g A : ℝ} (hg0 : 0 < g) (hg1 : g ≤ 1) (hA : 0 < A) (h : g ≤ (A / 64) ^ (4 / 3)) : g * |Real.log g| ^ 2 ≤ A

The α-free gate. γ ≤ (A/64)^{4/3} funds γ|log γ|² ≤ A.

theorem Algsuperdiff.Section4.Provider.Regularity.gamma_log_sq_le_rpow_quarter {g B : ℝ} (hg0 : 0 < g) (hg1 : g ≤ 1) (hB : 0 < B) (h : g ≤ (B / 64) ^ 2) : g * |Real.log g| ^ 2 ≤ B * g ^ (1 / 4)

The α-dependent gate. γ ≤ (B/64)² funds γ|log γ|² ≤ B·γ^{1/4} — the shape the Step-1 amplitude ε(δ) ≥ c·γ^{1/4} (a consequence of the root's own α-range α ≤ 1 - C√γ) consumes.