HomSpineRecutSupport

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

Support for the bundle re-cut: the multiscale clause alone, the printed

carriers' finiteness, and the numeral pin

What this file supplies

Route (i) is closed, leaving ONE mechanical step: re-cut the spine's per-ω bundle so that the transcribed source hypothesis appears with its MULTISCALE clause alone, and the Step-4 output hC4ex is PRODUCED rather than assumed. This file gives three of the ingredients that step needs.

1. THE FINITENESS CHECK (the CHECK-FIRST item). The re-cut carries four slot dominations; each is a genuine hypothesis only if its printed carrier can be ⊤. The verdict, machine-checked below:
   • parentTruncatedHomogenizationErrorInfinityOneScalar — NEVER ⊤ (CoarseGraining's …_eq_ofReal exhibits it as an ENNReal.ofReal), UNCONDITIONALLY;
   • parentTruncatedHomogenizationErrorInfinityTwoScalar — the same;
   • cubeEuclideanPositiveBesovOverlapESeminorm — never ⊤ on the printed data class MemCubeEuclideanFullWsp, which the root's own C^{0,1/2} binder supplies (HomCGFinalDatum.memCubeEuclideanFullWsp_of_holderHalf). So all three dominations are PINNABLE: at E:= carrier.toReal they hold by ENNReal.ofReal_toReal, and no printed finiteness requirement has to be added to the bundle. The three …_dominates_self lemmas below are that pinning, and they are what makes the re-cut bundle demonstrably non-vacuous.
2. The numeral pin. At the printed §4.5 exponent p = 4d and the display pin s₁′ = s/8, s′ = 7s/8, the joint conjunction s₁′ < s′ < s₂, s₂ < 1/2, 1/2 - d/p < s₂, s + d/p ≤ 1/2 is satisfied at s₂ = 3/8, for EVERY admissible s — and the guard itself is satisfiable (s = 1/8).

2. THE FINITENESS CHECK, and the pinning it licenses

theorem Algsuperdiff.Section4.Provider.Homogenization.parentErrorOne_ne_top {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (s1 : ↑HCPolySupport.FractionalOrder) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s1 ≠ ⊤

The 𝓔₁ carrier is never ⊤ — unconditionally. CoarseGraining's parentTruncatedHomogenizationErrorInfinityOneScalar_eq_ofReal exhibits it as an ENNReal.ofReal.

theorem Algsuperdiff.Section4.Provider.Homogenization.parentErrorTwo_ne_top {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (s1 : ↑HCPolySupport.FractionalOrder) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s1 ≠ ⊤

The 𝓔₂ carrier is never ⊤ — unconditionally.

theorem Algsuperdiff.Section4.Provider.Homogenization.overlapSeminorm_ne_top {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp Q s2 p g) : HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm Q s2 p g ≠ ⊤

The [𝐠] carrier is never ⊤ on the printed data class.

The overlap seminorm is below the dimension constant times the fractional seminorm, and both factors are finite on MemCubeEuclideanFullWsp.

theorem Algsuperdiff.Section4.Provider.Homogenization.parentErrorOne_dominates_self {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (s1 : ↑HCPolySupport.FractionalOrder) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s1 ≤ ENNReal.ofReal (HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s1).toReal

The 𝓔₁ domination is PINNABLE: at E₁:= carrier.toReal it is free.

theorem Algsuperdiff.Section4.Provider.Homogenization.parentErrorTwo_dominates_self {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (s1 : ↑HCPolySupport.FractionalOrder) : HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s1 ≤ ENNReal.ofReal (HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s1).toReal

The 𝓔₂ domination is PINNABLE: at E₂:= carrier.toReal it is free.

theorem Algsuperdiff.Section4.Provider.Homogenization.overlapSeminorm_dominates_self {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp Q s2 p g) : HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm Q s2 p g ≤ ENNReal.ofReal (HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm Q s2 p g).toReal

The [𝐠] domination is PINNABLE on the printed data class.

3. The numeral pin: p = 4d, s₁′ = s/8, s′ = 7s/8, s₂ = 3/8

def Algsuperdiff.Section4.Provider.Homogenization.recutExponent (d : ℕ) (hd : 1 ≤ d) : HCPolySupport.FiniteLpExponent

The printed §4.5 exponent p = 4d, as a FiniteLpExponent.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.recutExponent d hd = { exponent := ↑(4 * d), one_lt := ⋯, lt_top := ⋯ }

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.recutExponent_toReal (d : ℕ) (hd : 1 ≤ d) : (recutExponent d hd).exponent.toReal = 4 * ↑d

theorem Algsuperdiff.Section4.Provider.Homogenization.recutExponent_two_le (d : ℕ) (hd : 1 ≤ d) : 2 ≤ (recutExponent d hd).exponent

At the printed pin the exponent clears the 2 ≤ p threshold the display needs.