RootClauseBChain

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

1. The composite prefactor

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBCg (d : ℕ) (Ccacc Cosc CBc : ℝ) : ℝ

The Step-7c gradient-display constant C_g = 3^{3d+1/4}·C_cacc·(C_osc√C_lam+1) of StepSevenCaccFinalDisplay.

Equations

• Algsuperdiff.Section4.Provider.Regularity.rootClauseBCg d Ccacc Cosc CBc = Real.rpow 3 (3 * ↑d + 1 / 4) * Ccacc * (Cosc * √(256 / 63 * CBc) + 1)

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBPrefactor (d : ℕ) (Cch Ccacc Cosc CBc CB Ctr CWG CdM : ℝ) : ℝ

The clause-(B) prefactor, the composite constant the outer collapse produces: the oscillation half's C_g√C_cmp·(embedding·bridge·Poincaré·C_tr) plus the data half's C_g(√C_cmp·C_WG + C_dM), at C_cmp = 4.

Equations

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

2. Two scalar steps

theorem Algsuperdiff.Section4.Provider.Regularity.clauseB_const_mono {A P Cest R T : ℝ} (hR : 0 ≤ R) (hT : 0 ≤ T) (hP : P ≤ Cest) (h : A ≤ P * R * T) : A ≤ Cest * R * T

The final constant enlargement (RootAssemblyParameters §3's pattern).