OneStepBoundaryComposeGlue

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

The two structural glues of the boundary composition

Two mechanical pieces the boundary branch's assembly needs, and nothing else.

1. The H¹ algebra of the manuscript competitor

The boundary producer at the split datum takes the manuscript's odd competitor V_odd = v − ℓ_h − v₁ as a packaged H¹ realization vodd together with its weak harmonicity hvharm and the packaging identity heq. Both are supplied here from the chain's own data by the proved H¹ algebra: H1Function is an AddCommGroup (Homogenization.H1Function.sub_toFun/sub_grad), weak harmonicity is subtractive (AffineSplitHarmonic.isWeaklyHarmonicOn_sub) and the affine lift is weakly harmonic because its weak gradient is constant (AffineSplitHarmonic.isWeaklyHarmonicOn_affineLiftH1). No analytic input.

2. The affine-minimizer datum at the consumption window

The odd-class apparatus consumes IsAffineMinimizer U₂ V (c − A·x) A. On a truncated window this is a theorem, not a hypothesis: the window carries the axis-cube sandwich, hence the two-sided affine nondegeneracy, hence attainment (SandwichNondegeneracyAttainment through OneStepTriangle.exists_isAffineMinimizer_truncatedWindow). The only work here is the change of affine parametrization (c₀, g) ↦ (c₀ + g·x, g) that puts the minimizer in the (c − A·x, A) display the boundary producers print.

1. The H¹ glue: the packaged competitor v − ℓ_h − v₁

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_h1_oddCompetitor_affineSplit {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} {v v₁ : HCPolySupport.H1Function (truncatedWindow x m k)} (hv : Support.IsWeaklyHarmonicOn (truncatedWindow x m k) v) (hv₁ : Support.IsWeaklyHarmonicOn (truncatedWindow x m k) v₁) (cl : ℝ) (Al : HCPolySupport.Vec d) : ∃ (vodd : HCPolySupport.H1Function (truncatedWindow x m k)), Support.IsWeaklyHarmonicOn (truncatedWindow x m k) vodd ∧ ∀ (y : HCPolySupport.Vec d), vodd.toFun y = v.toFun y - affineLift x cl Al y - v₁.toFun y

The manuscript competitor as an H¹ datum.

V_odd = v − ℓ_h − v₁ is realized in H¹(U₂), is weakly harmonic there, and has the packaging identity, purely from the H¹ algebra: v and v₁ are weakly harmonic by hypothesis and the affine lift ℓ_h is weakly harmonic because its weak gradient is the constant A_ℓ.

2. The affine-minimizer datum at the consumption window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_isAffineMinimizer_shifted_truncatedWindow {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {V : HCPolySupport.Vec d → ℝ} (hV : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) : ∃ (c : ℝ) (A : HCPolySupport.Vec d), Support.IsAffineMinimizer (truncatedWindow x m k) V (c - HCPolySupport.vecDot A x) A

hmin at consumption. On the truncated window the affine minimum is attained, in the (c − A·x, A) parametrization the boundary producers print.