HomSpineInstallPins

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

The INSTALLED bundle: the four dominations discharged at the printed carriers

What this file supplies

The re-cut bundle's four slot dominations are PINNABLE but were not INSTALLED. This file installs them: the §4.5 bundle core is HomSpineRecutClose's re-cut bundle with

• the abstract slots Ccg, 𝓔₁, 𝓔₂, D_g REPLACED by the printed carriers' own toReal (recutPinnedDg and its three siblings);
• the four dominations, the four sign conditions and the two pin equations DELETED — they are discharged by HomSpineRecutSupport's _dominates_self corollaries at exactly those values;
• the order frame reduced to the two conditions that are not numerals: the bundle's own guard s + d/p ≤ 1/2 and the window 7s/8 < s₂.

What survives is the genuinely content-bearing core:

  { the MULTISCALE clause, hS, hlevel, hlevelDual, hEB/hdom, (jn, s, Cw, S, EB, Fflux) }.

The installation is general in (p, s₂) and is instantiated at the printed exponent p = 4d and the CORRECTED window pin s₂ = 49/100 (HomSpineInstallData machine-checks that the s₂ = 3/8 cannot absorb the forcing leg at the γ⁵ rate and that 49/100 can).

1. The display pin, as FractionalOrders

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutOrderLow (s : ↑HCPolySupport.FractionalOrder) : ↑HCPolySupport.FractionalOrder

The display pin's low order s₁′ = s/8 (the sharp choice).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.recutOrderLow s = ⟨↑s / 8, ⋯⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.recutOrderLow_val (s : ↑HCPolySupport.FractionalOrder) : ↑(recutOrderLow s) = ↑s / 8

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutOrderDual (s : ↑HCPolySupport.FractionalOrder) : ↑HCPolySupport.FractionalOrder

The display pin's dual order s′ = 7s/8 (the sharp choice: the carrier comparison's weight hypothesis holds with EQUALITY there).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.recutOrderDual s = ⟨7 * ↑s / 8, ⋯⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.recutOrderDual_val (s : ↑HCPolySupport.FractionalOrder) : ↑(recutOrderDual s) = 7 * ↑s / 8

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutOrderTop : ↑HCPolySupport.FractionalOrder

The CORRECTED window pin s₂ = 49/100. The earlier value s₂ = 3/8 is inside the membership band at p = 4d but fails the gap absorption's exponent condition (HomSpineInstallData machine-checks the failure). 49/100 is inside the band AND absorbs at the γ⁵ rate.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.recutOrderTop = ⟨49 / 100, Algsuperdiff.Section4.Provider.Homogenization.recutOrderTop._proof_5⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.recutOrderTop_val : ↑recutOrderTop = 49 / 100

2. The four printed carriers, at their own toReal

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutPinnedDg {d : ℕ} (m : ℤ) (s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The D_g slot, pinned to the printed positive-Besov overlap seminorm.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.recutPinnedDg m s2 p g = (HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm (HCPolySupport.originCube d m) s2 p g).toReal

theorem Algsuperdiff.Section4.Provider.Homogenization.recutPinnedDg_nonneg {d : ℕ} (m : ℤ) (s2 : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : 0 ≤ recutPinnedDg m s2 p g

5. The installation at the printed numeral pin

theorem Algsuperdiff.Section4.Provider.Homogenization.recutOrderTop_window (d : ℕ) (hd1 : 1 ≤ d) : ↑recutOrderTop < 1 / 2 ∧ 1 / 2 - ↑d / (recutExponent d hd1).exponent.toReal < ↑recutOrderTop

The corrected numeral pin is inside the membership band at p = 4d.