HomSeamSupClauseChain

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

The seam chain re-cut at the SUP-form multiscale clause

Why the clause slot moves

Step 3 is realized at the fixed exponent p = 4d, and the object the route actually produces is the manuscript's own sup-over-depths clause (HomSpineSupFormClause.CoarseGrainingSupMultiscale), supplied by HomSpineSupFormClause from the single-depth grid/smooth-dual comparison. The seam chain consumes the ℓ^p clause instead.

The swap is FREE at the point of consumption: HomSpineSupFormRethread.spineClauseC3_of_supMultiscale produces clause (C3) from the sup clause at IDENTICAL constants. This file carries that measurement through the four carriers of the seam chain:

  RecutCoreSupplyFluxAtSupGrad
  SpineDatumRecutCoreFluxAtHalfSupGrad      SpineDatumCoarseGrainingRecutFluxHalfSupGrad
  HomSpineClauseSupplierAtGrad              (unchanged -- the clause is gone by then)

Every declaration is the strict re-cut of its original: the fourth conjunct's ℓ^p-over-depths multiscale clause becomes CoarseGrainingSupMultiscale, and NOTHING else changes -- not a binder, not a constant, not an order. .toSup gives the regression (ℓ^p ⇒ sup), so nothing that was provable before becomes unprovable after.

1. The supply at the sup clause

def Algsuperdiff.Section4.Provider.Homogenization.RecutCoreSupplyFluxAtSupGrad {d : ℕ} (M : Section3.ABKModel d) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (Cen0 Ccg : ℝ) (hd1 : 1 ≤ d) (hlog : 4 ≤ |Real.log M.gamma|) (omega : Section3.Cutoff.CutoffSample d) : Prop

The gradient-threaded core supply, at the sup clause.

Equations

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

2. The twelve-conjunct core, at the sup clause

def Algsuperdiff.Section4.Provider.Homogenization.SpineDatumRecutCoreFluxAtHalfSupGrad {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (sb : { s : ℝ // 0 < s }) (sigmaBarM : ℝ) (hsig : 0 < sigmaBarM) (Kabs Ccg : ℝ) (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) (omega : Section3.Cutoff.CutoffSample d) : Prop

The gradient-threaded twelve-conjunct core, at the sup clause.

Equations

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

def Algsuperdiff.Section4.Provider.Homogenization.SpineDatumCoarseGrainingRecutFluxHalfSupGrad {d : ℕ} (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (sb : { s : ℝ // 0 < s }) (sigmaBarM : ℝ) (hsig : 0 < sigmaBarM) (Kabs : ℝ) (omega : Section3.Cutoff.CutoffSample d) : Prop

The gradient-threaded re-cut bundle, at the sup clause.

Equations

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

3. The installation, at the sup clause

theorem Algsuperdiff.Section4.Provider.Homogenization.spineDatumCoarseGrainingRecutFluxAtHalfSupGrad_of_core {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (sb : { s : ℝ // 0 < s }) {sigmaBarM Kabs Ccg : ℝ} (hsig : 0 < sigmaBarM) (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) (hs2lt : ↑s2 < 1 / 2) (hs2gt : 1 / 2 - ↑d / p.exponent.toReal < ↑s2) (hCcg0 : 0 ≤ Ccg) (hCcgDom : cgDualBoundConstFlux d p ≤ ENNReal.ofReal Ccg) (omega : Section3.Cutoff.CutoffSample d) (hcore : SpineDatumRecutCoreFluxAtHalfSupGrad M Cgap Y m sb sigmaBarM hsig Kabs Ccg p s2 omega) : SpineDatumCoarseGrainingRecutFluxHalfSupGrad M Cgap Y m sb sigmaBarM hsig Kabs omega

The bundle's installation from the core, at the sup clause.

theorem Algsuperdiff.Section4.Provider.Homogenization.spineDatumCoarseGrainingRecutFluxAtHalfSupGrad_of_core_pinned {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (sb : { s : ℝ // 0 < s }) {sigmaBarM Kabs Ccg : ℝ} (hsig : 0 < sigmaBarM) (hCcg0 : 0 ≤ Ccg) (hCcgDom : cgDualBoundConstFlux d (recutExponent d ⋯) ≤ ENNReal.ofReal Ccg) (omega : Section3.Cutoff.CutoffSample d) (hcore : SpineDatumRecutCoreFluxAtHalfSupGrad M Cgap Y m sb sigmaBarM hsig Kabs Ccg (recutExponent d ⋯) recutOrderTop omega) : SpineDatumCoarseGrainingRecutFluxHalfSupGrad M Cgap Y m sb sigmaBarM hsig Kabs omega

The same at the numeral pin.

4. The producer, at the sup clause

theorem Algsuperdiff.Section4.Provider.Homogenization.spineDatumRecutCoreFluxAtHalfSupGrad_of_supply {d : ℕ} [NeZero d] (hd1 : 1 ≤ d) (M : Section3.ABKModel d) {Cgap : ℝ} (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (hs : 0 < homS M) {Kabs Cen0 Ccg : ℝ} (hCcg0 : 0 ≤ Ccg) (omega : Section3.Cutoff.CutoffSample d) (hlog : 4 ≤ |Real.log M.gamma|) (hgamma1 : M.gamma < 1) (hCgap : 0 < Cgap) (hCen0 : 0 ≤ Cen0) (hfin : ethmB M Cgap Y m (homN M m) (homSeamBase M hs) omega ≠ ⊤) (hKabs : spineClauseConst d (homS M) (recutExponent d hd1).exponent.toReal (recutCwHalfFluxAt d hd1 M Ccg Cgap Cen0) (stepFourSchauderConstU d) ≤ Kabs) (hsupply : RecutCoreSupplyFluxAtSupGrad M Y m Cen0 Ccg hd1 hlog omega) : SpineDatumRecutCoreFluxAtHalfSupGrad M Cgap Y m (homSeamBase M hs) ↑(Section3.Annealed.sigmaBar M m) ⋯ Kabs Ccg (recutExponent d hd1) recutOrderTop omega

The core's producer from the supply, at the sup clause. The clause conjunct is a pure pass-through here, so the proof is the one verbatim.