RootClauseBGateBoundaryC1

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

1. The outer collapse with the H leg kept

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_collapse_boundary {E Kmain Kdata Ccol CdG CWG CWH CdM shomM gradLoc gradM dataG dataM W G H Lg Lh : ℝ} (hKmain : 0 ≤ Kmain) (hKdata : 0 ≤ Kdata) (hCcol : 0 ≤ Ccol) (hCWG : 0 ≤ CWG) (hCWH : 0 ≤ CWH) (hCdM : 0 ≤ CdM) (hE : 0 ≤ E) (hgradM : 0 ≤ gradM) (hLg : 0 ≤ Lg) (hLh : 0 ≤ Lh) (hWG0 : 0 ≤ W * G) (hWH0 : 0 ≤ W * H) (hdataM0 : 0 ≤ dataM) (hdataG : dataG ≤ CdG * Lg) (hWG : W * G ≤ CWG * Lg) (hWH : W * H ≤ CWH * Lh) (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 * H)) + dataM)) : gradLoc ≤ (Kmain * max 1 CdG + Kdata * (Ccol * CWG + Ccol * CWH + CdM)) * Real.rpow 3 E * (gradM + √shomM⁻¹ * Lg + √shomM * Lh)

The clause-(B) bracket collapse on the boundary branch.

RootClauseBArith.rootClauseB_collapse with H ≠ 0: the chain's data bracket splits as √σ_m^{-1}(W·G) + √σ_m(W·H), and the two dominations W·G ≤ C_WG·L_g, W·H ≤ C_WH·L_h carry it onto the printed three-leg bracket.

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

2. The (W, G, H) presentation that carries the boundary datum

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

The boundary presentation of the dataOsc slot.

RootClauseBArith.edFinalDataG_eq_dataOsc_scaled puts the interior data leg in the chain's slot at H = 0 and W = 4C_δC_gag/(1-r₁). The boundary leg cannot join that presentation without dividing by W, so the slot is entered at W = 1 instead, with the whole interior leg moved into G:

   edFinalDataG + dataH_∂  =  1 · ( σ_m^{-1}·(σ_m·edFinalDataG)  +  dataH_∂ ) .

A ring identity modulo σ_m·σ_m^{-1} = 1.

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

The W·G domination at the boundary presentation is an identity.

σ_m · edFinalDataG M C_δ (K_g C_gag) m = (4C_δC_gag/(1-r₁)) · 3^{m/2}K_g: the σ_m^{-1} of the Step-5 budget cancels against the σ_m introduced by the presentation, leaving the printed datum 3^{m/2}K_g at the budget's own weight. No estimate, no unit conversion.

noncomputable def Algsuperdiff.Section4.Provider.Regularity.boundaryCWH (d : ℕ) [NeZero d] (Cb C : ℝ) (k : ℕ) : ℝ

The seam constant C_WH = C_ah(1+C_gag)/(1-3^{-1/2}) + (4/log 3)·2C_bd.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.edBoundaryDataHPrinted_eq_boundaryCWH_mul (d : ℕ) [NeZero d] (Cb C : ℝ) (k : ℕ) (Kh : ℝ) (m : ℤ) : edBoundaryDataHPrinted d Cb C k Kh m = boundaryCWH d Cb C k * edFinalDataOscG Kh m

The unit-2 → unit-3 seam.

   dataH^print_∂ = ( C_ah(1+C_gag)/(1-3^{-1/2}) + (4/log 3)·2C_bd ) · 3^{m/2}K_h .

So the hWH slot of rootClauseB_display_gate_boundaryC1 is met at that explicit C_WH, with no estimate and no σ.

theorem Algsuperdiff.Section4.Provider.Regularity.boundaryCWH_nonneg (d : ℕ) [NeZero d] (Cb : ℝ) {C : ℝ} (hC : 0 ≤ C) (k : ℕ) : 0 ≤ boundaryCWH d Cb C k

The seam constant is nonnegative.