RootClauseBArith

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

1. Item (i): the origin cube's scale factor

theorem Algsuperdiff.Section4.Provider.Regularity.cubeScaleFactor_originCube_inv (d : ℕ) (k : ℤ) : (HCPolySupport.cubeScaleFactor (HCPolySupport.originCube d k))⁻¹ = 3 ^ (-k)

Item (i): the chain's oscHi normalization (cubeScaleFactor □_k)⁻¹ IS the 3^{-k} that's e.oscillation.Holder.bound prints.

2. Item (ii): the dataOsc presentation

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edFinalDataOscW {d : ℕ} (M : Section3.ABKModel d) (Cdel : ℝ) : ℝ

The dataOsc weight W = 4C_δ/(1 - r₁) of the interior Step-5 budget.

Equations

• Algsuperdiff.Section4.Provider.Regularity.edFinalDataOscW M Cdel = 4 * Cdel / (1 - Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioG M)

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edFinalDataOscG (Kg : ℝ) (m : ℤ) : ℝ

The dataOsc top-scale datum G = 3^{m/2}K_g.

Equations

• Algsuperdiff.Section4.Provider.Regularity.edFinalDataOscG Kg m = Real.rpow 3 (↑m / 2) * Kg

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

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalDataOscG_nonneg {Kg : ℝ} (hKg : 0 ≤ Kg) (m : ℤ) : 0 ≤ edFinalDataOscG Kg m

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalDataG_eq_dataOsc_scaled {d : ℕ} (M : Section3.ABKModel d) (Cdel Kg Cgag : ℝ) (m : ℤ) : edFinalDataG M Cdel (Kg * Cgag) m + 0 = edFinalDataOscW M Cdel * Cgag * ((↑(Section3.Annealed.sigmaBar M m))⁻¹ * edFinalDataOscG Kg m + 0)

Item (ii)'s own argument. The Step-6 interior endpoint states its data leg as edFinalDataG M C_δ (K_g·C_{S4.4}) m + 0, so the chain's dataOsc slot is met at the weight W = (4C_δ/(1-r₁))·C_{S4.4} and the printed datum G = 3^{m/2}K_g — the Gagliardo constant joins the W, not the leg, which is what puts the root's own 3^{m/2}K_g in the bracket. A ring identity.

3. Item (iv): the outer collapse onto the root's two legs

theorem Algsuperdiff.Section4.Provider.Regularity.bracket_pull_weight {A L W : ℝ} (hA : 0 ≤ A) (hL : 0 ≤ L) : A + W * L ≤ max 1 W * (A + L)

Pulling the interior budget's constant W out of the data leg: the printed bracket carries √σ_m^{-1}·3^{m/2}K_g with NO W, so W must join the prefactor. Abstract reals.

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_collapse {E Kmain Kdata Ccol CdG CWG CdM shomM gradLoc gradM dataG dataM W G Lg : ℝ} (hKmain : 0 ≤ Kmain) (hKdata : 0 ≤ Kdata) (hCcol : 0 ≤ Ccol) (hCWG : 0 ≤ CWG) (hCdM : 0 ≤ CdM) (hE : 0 ≤ E) (hgradM : 0 ≤ gradM) (hLg : 0 ≤ Lg) (hWG0 : 0 ≤ W * G) (hdataM0 : 0 ≤ dataM) (hdataG : dataG ≤ CdG * Lg) (hWG : W * G ≤ CWG * Lg) (hdataM : dataM ≤ CdM * (√shomM⁻¹ * Lg)) (h : gradLoc ≤ Kmain * Real.rpow 3 E * (gradM + √shomM⁻¹ * dataG) + Kdata * Real.rpow 3 (3 / 4 * E) * (Ccol * (W * ((√shomM)⁻¹ * G + √shomM * 0)) + dataM)) : gradLoc ≤ (Kmain * max 1 CdG + Kdata * (Ccol * CWG + CdM)) * Real.rpow 3 E * (gradM + √shomM⁻¹ * Lg)

Item (iv): the clause-(B) bracket collapse.

's outer collapse in the shape the concrete carriers need. The Step-7 end chain concludes

  gradLoc ≤ Kmain·3^E·(gradM + √σ_m^{-1}·dataG)
          + Kdata·3^{3E/4}·(Ccol·(W·((√σ_m)^{-1}·G + √σ_m·H)) + dataM) ,

with H = 0 on the interior branch, and e.energy.density.estimate prints ONE power of three and the SINGLE data leg Lg = 3^{m/2}K_g. Three DOMINATIONS collapse the former onto the latter — the Poincaré-leg datum (dataG ≤ CdG·Lg), the oscillation-leg datum (W·G ≤·Lg) and the Caccioppoli's own data leg (dataM ≤ CdM·√σ_m^{-1}·Lg) — together with the parent's own exponent step 3^{3E/4} ≤ 3^E (RootAssemblyChain.rpow_three_threeQuarter_le).

Pure arithmetic: every domination is a hypothesis, Real.rpow is opaque throughout, and no estimate is derived.