HomSeamEnergySlotAssembly

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

The energy conjuncts of the seam residue, assembled at the enlarged Y

What this file supplies

The seam residue's energy supply asks, per ω and per printed elliptic pair, for {0 ≤ S, the partial-sum slot, hSbound} plus the multiscale clause. This file produces the FIRST THREE from the Theorem-C display, by supplying the step no file supplies:

  HomProviderBAssembly.RegularityDisplayAt   ⟶   HomSpineEnergyDensity.RegularityEnergyDisplay

(regularityEnergyDisplay_of_regularityDisplayAt), and then composing HomSpineTopScale.htop_of_stepTwoA_enlargedY with HomSpineEnergySlot.energySlot_of_regularityDisplay at the seam's own Y slot.

The two binder mismatches the slice resolves (both DISPLAYED, neither assumed

away)

1. The K_h^∞ gate. The display's own sup binder is ‖∇h‖ ≤ 3^{m/2}K_h, while the seam's per-ω datum carries the root's ‖∇h‖ ≤ K_h^∞ with a FREE K_h. The slice runs the display at the shifted constant seamShiftedKh m K_h K_h^∞ = 3^{-m/2}K_h^∞ + K_h, at which 3^{m/2}·K_h' = K_h^∞ + 3^{m/2}K_h — so the bracket's third term is EXACTLY the printed energyBracket's second summand. Nothing is lost: running htop at (K_h:= K_h', K_h^∞:= 0) returns the printed bracket on the nose (energyBracket_zero_seamShiftedKh).

2. HasGradientOn. The anomalous_regularity display carries the classical-gradient binder HasGradientOn □_m h.toFun h.grad (the V3 amendment). The frozen ROOT carries it too, but the spine drops it (the §4.5 provider introduces it and discards it), so the per-ω residues do NOT bind it. Every theorem below therefore takes it as an EXPLICIT hypothesis: the energy slot is available exactly for the pairs the theorem speaks about.

1. The shifted Hölder constant of the sup binder

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.seamShiftedKh (m : ℤ) (Kh KhInf : ℝ) : ℝ

The display's Hölder constant at the root's own sup binder.

The display gates its data by ‖∇h‖_{L^∞} ≤ 3^{m/2}K_h; the root binds ‖∇h‖_{L^∞} ≤ K_h^∞ with an independent K_h. Running the display at 3^{-m/2}K_h^∞ + K_h meets the gate and reproduces the printed bracket.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.seamShiftedKh m Kh KhInf = Real.rpow 3 (-(↑m / 2)) * KhInf + Kh

theorem Algsuperdiff.Section4.Provider.Homogenization.seamShiftedKh_nonneg {m : ℤ} {Kh KhInf : ℝ} (hKh : 0 ≤ Kh) (hKhInf : 0 ≤ KhInf) : 0 ≤ seamShiftedKh m Kh KhInf

theorem Algsuperdiff.Section4.Provider.Homogenization.le_seamShiftedKh {m : ℤ} {Kh KhInf : ℝ} (hKhInf : 0 ≤ KhInf) : Kh ≤ seamShiftedKh m Kh KhInf

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_mul_seamShiftedKh (m : ℤ) (Kh KhInf : ℝ) : Real.rpow 3 (↑m / 2) * seamShiftedKh m Kh KhInf = KhInf + Real.rpow 3 (↑m / 2) * Kh

The shift is exact: the weight 3^{m/2} applied to the shifted constant is the printed sum K_h^∞ + 3^{m/2}K_h.

theorem Algsuperdiff.Section4.Provider.Homogenization.energyBracket_zero_seamShiftedKh (sigma : ℝ) (m : ℤ) (Kg Kh KhInf : ℝ) : energyBracket sigma (Real.rpow 3 (↑m / 2)) Kg 0 (seamShiftedKh m Kh KhInf) = energyBracket sigma (Real.rpow 3 (↑m / 2)) Kg KhInf Kh

The printed bracket at K_h^∞ = 0 and the shifted constant IS the printed bracket at the root's own pair. This is the identity that makes the K_h^∞ gate free.

2. The bracket is finite

theorem Algsuperdiff.Section4.Provider.Homogenization.regularityDataBracket_ne_top {d : ℕ} (M : Section3.ABKModel d) {m : ℤ} (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {sigmaBarM Kg Kh : ℝ} (hKg : 0 ≤ Kg) (hKh : 0 ≤ Kh) : regularityDataBracket M m u sigmaBarM Kg Kh ≠ ⊤

The Theorem-C bracket is never ⊤ on the printed data signs.

3. THE SLICE: the display, cut at one finite minimal scale

theorem Algsuperdiff.Section4.Provider.Homogenization.regularityEnergyDisplay_of_regularityDisplayAt {d : ℕ} (M : Section3.ABKModel d) {Creg alpha : ℝ} {m : ℤ} {X : Section3.Cutoff.CutoffSample d → ℕ∞} {omega : Section3.Cutoff.CutoffSample d} (hdisp : RegularityDisplayAt M Creg alpha m X omega) {k : ℕ} (hXk : X omega = ↑k) {L : ℤ} (hL : m ≤ L) {u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg Kh KhInf : ℝ} (hKh : 0 ≤ Kh) (hKhInf : 0 ≤ KhInf) (hsol : Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g) (hKgB : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g) (hKhB : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad) (hsup : ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) (hgrad : Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad) : RegularityEnergyDisplay M m k u Creg alpha (regularityDataBracket M m u (↑(Section3.Annealed.sigmaBar M m)) Kg (seamShiftedKh m Kh KhInf))

THE MISSING LINK.

HomProviderBAssembly.RegularityDisplayAt — the byte transcription of anomalous_regularity's per-ω body — sliced into HomSpineEnergyDensity.RegularityEnergyDisplay at one sample, one admissible L, one elliptic pair and one FINITE value k of the minimal scale.

Both binder mismatches of the module docstring are resolved in the statement: the sup gate is met at seamShiftedKh, and hgrad is the theorem's own classical-gradient binder.

4. The pinned top-scale constant

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.seamTopScaleConst (d : ℕ) (Cstep : ℝ) : ℝ

THE PINNED C_top OF THE SEAM.

HomSpineTopScale.htop_of_stepTwoA_enlargedY's own constant at the consumer pin t = 1/4 and at the discharged data-bridge constant HomSpineDataBridge.stepTwoDataConstPinned. Model-free: d, the Step-2 constant, and nothing else.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.seamTopScaleConst d Cstep = 10 * Cstep * √(2 * ↑d) * Algsuperdiff.Section4.Provider.Homogenization.stepTwoDataConstPinned d + 1

theorem Algsuperdiff.Section4.Provider.Homogenization.seamTopScaleConst_nonneg (d : ℕ) {Cstep : ℝ} (hCstep : 0 ≤ Cstep) : 0 ≤ seamTopScaleConst d Cstep

theorem Algsuperdiff.Section4.Provider.Homogenization.seamTopScaleConst_eq (d : ℕ) (Cstep : ℝ) : Cstep * ((1 / 4).rpow (-(3 / 2)) + (1 / 4).rpow (-(1 / 2))) * √(2 * ↑d) * stepTwoDataConstPinned d + 1 = seamTopScaleConst d Cstep

The symbolic constant of htop_of_stepTwoA_enlargedY at t = 1/4 and the pinned data constant IS seamTopScaleConst.

5. The Y-slot identification

theorem Algsuperdiff.Section4.Provider.Homogenization.seamEnlargedY_apply_of_eq_coe {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {Ctop alpha : ℝ} (hCtop : 0 ≤ Ctop) {X : Section3.Cutoff.CutoffSample d → ℕ∞} (omega : Section3.Cutoff.CutoffSample d) {k : ℕ} (hXk : X omega = ↑k) : seamEnlargedY M m Ctop (homMinimalScaleFactor (1 - alpha) X) omega = ENNReal.ofReal (Ctop * 3 ^ ((1 - alpha) * ↑k)) * stepTwoEnlargedY M m ⋯ omega

THE SEAM's Y SLOT IS htop's Y SLOT, at every sample where the minimal scale is finite. The ℕ∞ cut is the only content: off it homMinimalScaleFactor is ⊤ and the printed factor carries no information.

6. htop at the seam's own Y

theorem Algsuperdiff.Section4.Provider.Homogenization.seamQuarterPos : 0 < 1 / 4

theorem Algsuperdiff.Section4.Provider.Homogenization.htop_seamEnlargedY (d : ℕ) [NeZero d] (hd1 : 1 ≤ d) : ∃ (Cstep : ℝ), 0 < Cstep ∧ ∀ (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg Kh KhInf alpha : ℝ} {X : Section3.Cutoff.CutoffSample d → ℕ∞} {k : ℕ}, m ≤ L → X omega = ↑k → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Support.fluxCorrectedError M L m (1 / 4 / 2) omega = Support.fluxCorrectedErrorRepresentative M L m ⟨1 / 4 / 2, ⋯⟩ omega → Support.fluxCorrectedError M L m (1 / 4) omega = Support.fluxCorrectedErrorRepresentative M L m ⟨1 / 4, seamQuarterPos⟩ omega → Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨1 / 4 / 2, ⋯⟩ omega ≠ ⊤ → Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨1 / 4, seamQuarterPos⟩ omega ≠ ⊤ → Support.fluxCorrectedTwoScaleErrorObservableSup M m m homQuarter omega ≠ ⊤ → 0 ≤ Kg → 0 ≤ Kh → 0 ≤ KhInf → 3 ^ ((1 - alpha) * ↑k) * (regularityDataBracket M m u (↑(Section3.Annealed.sigmaBar M m)) Kg (seamShiftedKh m Kh KhInf)).toReal ≤ recutEnergyFactor M (seamEnlargedY M m (seamTopScaleConst d Cstep) (homMinimalScaleFactor (1 - alpha) X)) m omega * energyBracket (↑(Section3.Annealed.sigmaBar M m)) (Real.rpow 3 (↑m / 2)) Kg KhInf Kh

htop, AT THE SEAM's OWN Y SLOT.

HomSpineTopScale.htop_of_stepTwoA_enlargedY instantiated at the consumer pin t = 1/4, at the DISCHARGED data bridge (HomSpineDataBridge.stepTwoDataBridge_of_holder_pinned, so is not an input here), at the shifted Hölder constant and at K_h^∞ = 0 — the last choice is what makes the right-hand bracket the PRINTED energyBracket σ_m 3^{m/2} K_g K_h^∞ K_h with no slack at all.

7. THE THREE ENERGY CONJUNCTS, PRODUCED

theorem Algsuperdiff.Section4.Provider.Homogenization.seamEnergySlot_of_regularityDisplayAt (d : ℕ) [NeZero d] (hd1 : 1 ≤ d) : ∃ (Cstep : ℝ), 0 < Cstep ∧ ∀ (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {X : Section3.Cutoff.CutoffSample d → ℕ∞} {k : ℕ} {Creg : ℝ}, 0 < Creg → 4 ≤ |Real.log M.gamma| → X omega = ↑k → RegularityDisplayAt M Creg (homAlpha M) m X omega → ∀ (L : ℤ), m ≤ L → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → Support.fluxCorrectedError M L m (1 / 4 / 2) omega = Support.fluxCorrectedErrorRepresentative M L m ⟨1 / 4 / 2, ⋯⟩ omega → Support.fluxCorrectedError M L m (1 / 4) omega = Support.fluxCorrectedErrorRepresentative M L m ⟨1 / 4, seamQuarterPos⟩ omega → Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨1 / 4 / 2, ⋯⟩ omega ≠ ⊤ → Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨1 / 4, seamQuarterPos⟩ omega ≠ ⊤ → Support.fluxCorrectedTwoScaleErrorObservableSup M m m homQuarter omega ≠ ⊤ → ∃ (S : ℝ), 0 ≤ S ∧ (∀ (N : ℕ), coarseGrainingEnergyPartial (HCPolySupport.originCube d m) (recutExponent d hd1).exponent.toReal (homS M - homS M / 4) (homK M) N (printedLocalEnergy (Support.fluxCorrectedCoeffOn M L m (HCPolySupport.originCube d m) omega) u) ≤ S) ∧ S ≤ recutEnergySlotConst Creg (homAlpha M) (recutExponent d hd1).exponent.toReal (homS M) (homK M) * recutEnergyFactor M (seamEnlargedY M m (seamTopScaleConst d Cstep) (homMinimalScaleFactor (1 - homAlpha M) X)) m omega * energyBracket (↑(Section3.Annealed.sigmaBar M m)) (Real.rpow 3 (↑m / 2)) Kg KhInf Kh

{0 ≤ S, the partial-sum slot, hSbound} OF THE SEAM RESIDUE, PRODUCED.

The first three conjuncts of the seam's energy residue at its own enlarged Y, from the Theorem-C display alone. The partial-sum slot is delivered at the PRINTED coefficient ã_{L,m}: by HomSeamFluxCoefficient.printedLocalEnergy_fluxCorrected the energy functional is the SAME function of cubes at ã_{L,m} and at a_L, so no estimate is spent on the swap.

Two hypotheses are visible here that the residue statement does NOT bind (module docstring, mismatches (1) and (2)): the classical-gradient binder hgrad of the theorem, and the finiteness X ω = k of the minimal scale. The C_en⁰ slot produced is recutEnergySlotConst Creg (homAlpha M) (4d) (homS M) (homK M) — it names Creg and the model, and its coarseGrainingGeomFactor (4d) (homS M / 4) factor is's D3.