HomSpineEnergySlot

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

The §4.5 supplier's energy slot, produced from Theorem C

What this file supplies

The supplier asks, per ω and per elliptic pair, for a real S with

  0 ≤ S,     ∀ N, coarseGrainingEnergyPartial □_m p (s - s/4) j_n N Gen ≤ S,
  S ≤ C_en · recutEnergyFactor · energyBracket σ_m 3^{m/2} K_g K_h^∞ K_h

at Gen:= printedLocalEnergy (the cutoff field's own per-cell energy). This is the Theorem-C item of the §4.5 spine. energySlot_of_regularityDisplay produces all three from

1. HomSpineEnergyDensity.RegularityEnergyDisplay — Theorem C's first conjunct, sliced (deep range only; the shallow range is recovered inside printedLocalEnergy_le_of_display by the sub-cube average step);
2. the printed order identification 1 - α = s/2 (the §4.5 web's own pin, which is what makes the s₁ = s/4 weight gap positive — see coarseGrainingEnergyPartial_le_at_quarterPin);
3. htop — the top-scale datum, the ONE remaining input: the minimal-scale factor times Theorem C's own three-term bracket is below the printed Step-2 random factor 3^{(1-α)X_m(α)}(1 + 𝓔_{1/4}) times the printed data bracket. That is exactly the printed display's constant shape; the Y slot of recutEnergyFactor carries 3^{(1-α)X_m(α)} and the (1 + 𝓔_{1/4}) factor absorbs the bracket's own top-scale energy √ν‖∇u‖_{L²(□_m)} against the BoundsMathcalEaL datum. It is stated explicitly, not assumed away.

The constant

recutEnergySlotConst is the deterministic half of C_en: the Theorem-C constant, the mesoscale depth factor 3^{(1-α)j_n} at the j_n = homK M pin, and the finite-p geometric factor (1 - 3^{-(s/4)p})^{-1/p} the ℓ^p slot pays over the p = ∞ sup. No randomness, no ν, no σ.

1. One piece of bookkeeping

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingGeomFactor_nonneg {p w : ℝ} (hp : 0 < p) (hw : 0 < w) : 0 ≤ coarseGrainingGeomFactor p w

The finite-p geometric factor is nonnegative on the printed window.

2. The deterministic half of the Step-2 constant

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutEnergySlotConst (Creg alpha p s : ℝ) (jn : ℕ) : ℝ

The deterministic Step-2 constant of the energy slot.

The Theorem-C constant C, the mesoscale depth factor 3^{(1-α)j_n}, and the finite-p geometric factor. Model-independent: no ω, no ν, no σ.

Equations

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

3. The Step-2b family bound at the s₁ = s/4 pin

theorem Algsuperdiff.Section4.Provider.Homogenization.printedLocalEnergy_le_family {d : ℕ} {M : Section3.ABKModel d} {m : ℤ} {X : ℕ} {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {Creg alpha : ℝ} {T : ENNReal} (hdisp : RegularityEnergyDisplay M m X u Creg alpha T) (hT : T ≠ ⊤) (halpha1 : alpha ≤ 1) (hCreg : 0 ≤ Creg) {s : ℝ} (halpha : 1 - alpha = s / 2) (L : ℤ) (omega : Section3.Cutoff.CutoffSample d) (jn i : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) (jn + i)) : printedLocalEnergy (Section3.Cutoff.coefficientCutoffCoeffOn M L omega (HCPolySupport.originCube d m)) u R ≤ Creg * 3 ^ ((1 - alpha) * ↑X) * 3 ^ ((1 - alpha) * ↑jn) * T.toReal * 3 ^ (s / 2 * ↑i)

The printed family bound.

At depth j_n + i below □_m the per-cube energy grows at most like 3^{(s/2)i} — the §4.5 web's 1 - α = s/2 — off the depth-j_n value. This is the exact hypothesis coarseGrainingEnergyPartial_le_at_quarterPin consumes.

4. THE ENERGY SLOT

theorem Algsuperdiff.Section4.Provider.Homogenization.energySlot_of_regularityDisplay {d : ℕ} {M : Section3.ABKModel d} {m : ℤ} {X : ℕ} {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {Creg alpha : ℝ} {T : ENNReal} {Y : Section3.Cutoff.CutoffSample d → ENNReal} {sigmaBarM pow Kg KhInf Kh p s : ℝ} (hdisp : RegularityEnergyDisplay M m X u Creg alpha T) (hT : T ≠ ⊤) (halpha1 : alpha ≤ 1) (hCreg : 0 ≤ Creg) (halpha : 1 - alpha = s / 2) (hp : 0 < p) (hs : 0 < s) (L : ℤ) (omega : Section3.Cutoff.CutoffSample d) (jn : ℕ) (htop : 3 ^ ((1 - alpha) * ↑X) * T.toReal ≤ recutEnergyFactor M Y m omega * energyBracket sigmaBarM pow Kg KhInf Kh) : ∃ (S : ℝ), 0 ≤ S ∧ (∀ (N : ℕ), coarseGrainingEnergyPartial (HCPolySupport.originCube d m) p (s - s / 4) jn N (printedLocalEnergy (Section3.Cutoff.coefficientCutoffCoeffOn M L omega (HCPolySupport.originCube d m)) u) ≤ S) ∧ S ≤ recutEnergySlotConst Creg alpha p s jn * recutEnergyFactor M Y m omega * energyBracket sigmaBarM pow Kg KhInf Kh

hS0, hS and hSbound, produced.

The three energy conjuncts of the supplier from the Theorem-C display, the printed order identification 1 - α = s/2, and the disclosed top-scale datum. The majorant is the printed one: the deterministic Step-2 constant times 3^{(1-α)X_m(α)}(1 + 𝓔_{1/4}) times the data bracket.