HomSeamSupClauseSpine

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

The clause supplier and the budgeted supply layers, at the SUP-form clause

What this file supplies

HomSeamSupClauseChain re-cut the seam carriers at the sup-form multiscale clause. This file carries the re-cut to the spine's clause supplier — the last place the clause is visible — and states the budgeted seam bundle of the gradient provider at the sup carriers:

  homSpineClauseSupplierAtGrad_of_datumRecutFluxHalfSupGrad
  SeamBundleOfRegularityHalfSupGradBudget

The supplier's proof is the same, with EXACTLY ONE token changed: clause (C3) now runs through HomSpineSupFormRethread.spineClauseC3_of_supMultiscale. Its argument list, its output constant 96 d² · liftGeomFactor (s + d/p) · C_w and clause (C4) are untouched — that is the losslessness measurement, executed.

1. The clause supplier, from the SUP-form datum

theorem Algsuperdiff.Section4.Provider.Homogenization.homSpineClauseSupplierAtGrad_of_datumRecutFluxHalfSupGrad {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : Section3.ABKModel d) (Cgap : ℝ) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (sb : { s : ℝ // 0 < s }) {sigmaBarM Kabs : ℝ} (hsig : 0 < sigmaBarM) (omega : Section3.Cutoff.CutoffSample d) (hcg : SpineDatumCoarseGrainingRecutFluxHalfSupGrad M Cgap Y m sb sigmaBarM hsig Kabs omega) : HomSpineClauseSupplierAtGrad M Cgap Y m sb sigmaBarM Kabs omega

THE SPINE'S CLAUSE SUPPLIER, FROM THE SUP-FORM DATUM.

The spine's clause supplier at the gradient binder, with the multiscale conjunct read at the print's own sup aggregation. Clause (C3) now runs through spineClauseC3_of_supMultiscale at the IDENTICAL constant; clause (C4) never sees the aggregation at all.

2. The budgeted seam bundle at the sup carriers

def Algsuperdiff.Section4.Provider.Homogenization.SeamBundleOfRegularityHalfSupGradBudget (d : ℕ) (cstar gamma0 Cgap : ℝ) (KabsF : Section3.ABKModel d → ℝ) (Ctop Creg : ℝ) : Prop

The budgeted gradient seam bundle at the sup-form datum.

Equations

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