HomSpineRecutClose #

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

Theorem B, §4.5: THE BUNDLE RE-CUT — the multiscale clause alone #

What changes #

HomSpineRepClose.SpineDatumCoarseGrainingGauge carries the transcribed source hypothesis hCG' at ALL THREE of its clauses and the Schauder external's Step-4 output hC4ex as an item. The two DUALITY clauses and hC4ex are PRODUCIBLE from the root's own binders. This module performs the resulting re-cut:

  the re-cut bundle  =  SpineDatumCoarseGrainingGauge
      with  hCG'   ↦  its MULTISCALE clause alone
      with  hC4ex  DELETED
      plus  the four slot dominations + hlevelDual, at the display pin
            s₁′ = s/8, s′ = 7s/8, with Gen:= printedLocalEnergy.

the two duality clauses come from the printed display through the two duality slots at the spine's own cutoff pair, whose own inputs are the root's two IsDirichletSolutionOn binders and the root's C^{0,1/2} binder on 𝐠;
hC4ex comes from the Step-4 comparator-energy producer — the external supplies the comparator, and the three H¹-level integrability facts are PRODUCED here (memVectorL2_coeffFlux), not assumed;
the four slot dominations are the price of route (i): they tie the bundle's abstract numbers Ccg, 𝓔₁, 𝓔₂, D_g to the printed carriers of the display. HomSpineRecutSupport machine-checks that every one of those carriers is FINITE, so each domination is satisfiable by pinning the number to the carrier's own toReal. No printed finiteness requirement survives.

The order pin, and why it is forced #

HomCGCarrierEnergy's comparison needs wgap ≤ s′ - s₁′, and the bundle's own wgap is s - s/4 = 3s/4. The pin s₁′ = s/8, s′ = 7s/8 meets it with EQUALITY, and the order loss s - s′ = s/8 keeps the duality window 0 < (s-s′)p′ < d open. The per-site reading is the disposition of the correction.

The final conditional set is still exactly two entries #

htail — the Theorem-C minimal-scale tail, a declared dependency edge (Theorem C), not an internal §4.5 obligation;
hcg — the per-ω re-cut bundle, whose items are the MULTISCALE clause of hCG' (a declared source hypothesis), the energy slot hS, the level conditions hlevel/hlevelDual, the four slot dominations, hEB/hdom, and the numerical frame. NO duality clause, NO hC4ex, NO frame item.

1. The three `H¹`-level integrability facts, PRODUCED #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.memVectorL2_coeffFlux {d : ℕ} {Q : HCPolySupport.TriadicCube d} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) :

HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a.toCoeffField x) (u.grad x)

The flux of an H¹ function against a Chapter-2 coefficient is L².

The public coefficient object is only a.e.-elliptic, so the proof passes to the internal pointwise-good representative and transports back — CoarseGraining's own route for Solution.flux_memVectorL2, here for a bare H¹ function.

source