HomSpineResidueCore #

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

The re-cut core, produced: all twelve conjuncts at the corrected pin #

What this file supplies #

HomSpineInstallPins installs the twelve-conjunct core of the §4.5 bundle. All twelve conjuncts are available at the corrected numeral pin p = 4d, s = |log γ|⁻¹, s₂ = 49/100, j_n = ⌈10|log γ|⌉, from one per-ω supplier and a frame condition on K_abs:

conjunct	where it comes from
`0 < j_n`, the guard, the window, `0 ≤ C_w`	the numeral pin (proved here)
`spineClauseConst … ≤ K_abs`	`hKabs`, a frame condition on the free `K_abs`
`0 ≤ E_B`, `ofReal E_B ≤ EthmB(m)`	the real cut of `EthmB(m)` (proved here)
the MULTISCALE clause	the supplier (the coarse-graining input)
`0 ≤ S`, the partial sums	the supplier
`hlevel`, `hlevelDual`	`HomSpineResidueLevel` (the `EthmB(m)` pairing)

So the residual bill of Theorem B's §4.5 spine is exactly that supplier plus hfin and hKabs.

The residual bill, itemized #

The supplier asks, for each L ≥ m and each printed elliptic pair, for

the energy partial-sum slot S with the printed bound hSbound at the Step-2 constant shape C · 3^{(1-α)X_m}(1 + 𝓔_{1/4}) — this is the Theorem-C item;
the MULTISCALE coarse-graining clause at Gen:= printedLocalEnergy;
the two 𝓔-dominations — the carrier seam, disclosed in HomSpineResiduePairing and NOT dischargeable at the current pins.

hfin is the a.e. finiteness of the [0,∞] carrier, which HomSpineFinalWitness already derives from the p = 1 moment.