HomSeamGradSpine

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

The clause supplier and the spine endpoint, re-threaded at the gradient binder

What this file supplies

The display's classical-gradient binder is threaded through the supply and the twelve-conjunct core. This file carries it the rest of the way to the spine's clause supplier:

  HomSpineClauseSupplierAtGrad                     -- the supplier, gated

Each is the strict re-threading of its original: the binder list of the per-omega body gains

  HasGradientOn (openCubeSet (originCube d m)) h.toFun h.grad ->

after the KhInf sup binder, and the proof passes it straight through. The E_B witness, the two moment clauses and the sigmaBar clause of the endpoint are BINDER-FREE and are re-used, not re-proved.

1. The clause supplier, gated

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

The spine's clause supplier with the display's classical-gradient binder threaded through.

Equations

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