RootClauseBFinalRegime

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

1. The bundle

structure Algsuperdiff.Section4.Provider.Regularity.RootClauseBGammaFacts {d : ℕ} (M : Section3.ABKModel d) (C Cann Cind C1 Crg : ℝ) : Prop

Every γ-regime clause the clause-(B) chain consumes, at one model.

C is the Step-6 producer's regime constant, C_ann its annular companion, C_ind the all-scales induction-state constant, C₁ the Step-1 constant the display is stated at, and C_rg the constant of the printed α-range.

• ltHalf : M.gamma < 1 / 2

  γ < 1/2: the standing Step-5 ratio gate.

• leQuarter : M.gamma ≤ 1 / 4

  γ ≤ 1/4: the M-uniform funding enlargement's gate.

• le256 : M.gamma ≤ 1 / 256

  γ ≤ 1/256: the Step-6 producer's own numeral.

• regimeC : M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10

  The Step-6 producer's first regime clause.

• regimeAnn : M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10

  The Step-6 producer's annular regime clause.

• regimeInd : M.gamma ≤ Cind⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10

  The induction-state regime clause.

• floorEight : 8 * M.gamma ≤ stepOneSEighth

  The Step-1 floor 8γ ≤ s/8 of the A6 cap producer.

• smallFree : M.gamma * |Real.log M.gamma| ^ 2 ≤ (stepOneS / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (C⁻¹ * stepOneS ^ 4)

  The α-free γ|log γ|² gate of the Step-6 producer.

• smallEp (alpha : ℝ) : 0 < alpha → alpha ≤ 1 - Crg * √M.gamma → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta C1 alpha)

  The α-dependent γ|log γ|² gate, at every α in the printed range.

2. The two scalar thresholds

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBGateFree (cstar C : ℝ) : ℝ

The right-hand side of the α-free gate, as a positive constant.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBGateEp (cstar C1 Crg : ℝ) : ℝ

The γ^{1/4}-coefficient of the α-dependent gate, as a positive constant.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBGateFree_pos {cstar C : ℝ} (hcstar : 0 < cstar) (hC : 0 < C) : 0 < rootClauseBGateFree cstar C

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBGateEp_pos {cstar C1 Crg : ℝ} (hcstar : 0 < cstar) (hC1 : 0 < C1) (hCrg : 0 < Crg) : 0 < rootClauseBGateEp cstar C1 Crg

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneEp_ge_rpow_quarter {C1 Crg g alpha : ℝ} (hC1 : 0 < C1) (hCrg : 0 < Crg) (hg : 0 < g) (halpha : alpha ≤ 1 - Crg * √g) : stepOneSEighth * √(C1⁻¹ * Crg) * g ^ (1 / 4) ≤ stepOneEp (stepOneDelta C1 alpha)

The Step-1 amplitude at the printed α-range: ε(δ) ≥ (s/8)√(C₁⁻¹C)γ^{1/4}.

3. The producer

theorem Algsuperdiff.Section4.Provider.Regularity.exists_rootClauseBGammaFacts (d : ℕ) {cstar C Cann Cind C1 Crg : ℝ} (hcstar : 0 < cstar) (hC : 0 < C) (hCann : 0 < Cann) (hCind : 0 < Cind) (hC1 : 0 < C1) (hCrg : 0 < Crg) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → RootClauseBGammaFacts M C Cann Cind C1 Crg

One γ₀ for the whole clause-(B) chain.

The threshold is the minimum of the printed numeral 1/256, the three c⋆¹⁰-regimes, and the two γ|log γ|² thresholds of RootClauseBFinalArith §4. Every clause of RootClauseBGammaFacts then holds for every model in the regime, and the α-dependent one holds at every α of the printed range.