OneStepOddPackaging

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

The H¹ packaging of the odd extension

• hasWeakGradientOn_oddFaceExtend_of_localizedZeroTrace — the analytic core: on a reflection-symmetric open U, the odd extension W = Z − Z ∘ r of the zero extension Z of v ∈ H¹(faceHalf U i a σ) has the weak gradient oddFaceExtendGrad a i (zeroExtendGrad … v.grad) on all of U — the interface hyperplane contributes nothing, provided v has face-only zero trace (LocalizedZeroTraceFunctionOn (faceHalf U i a σ) U). Per test φ and coordinate j, the change of variables folds the test to ψⱼ = φ − εⱼ·(φ ∘ r) (εⱼ = −1 exactly at the normal coordinate), and the eta-cutoff integration by parts of OneStepOddPackagingCore closes the identity; for j = i the fold is the even fold φ + φ ∘ r, which does not vanish on the interface — that is precisely where the zero trace is spent.

• exists_h1Function_oddFaceExtend — the packaged existence: an H1Function U whose toFun/grad are pointwise the odd extension pair, i.e. verbatim the hwval (at c₀ = 0) and hwgrad slots the boundary branch's odd producer asks for at one met face, and the hw slot of the proved transfers.

• localizedZeroTraceFunctionOn_oddFaceExtend — the stage-to-stage transport: the odd extension inherits face-only zero trace on the larger box, from the three H¹₀ closure facts of the core module. This is what lets the multi-face iteration (OneStepPartialReflection) re-fold across the next met face.

• exists_h1_oddFaceReflection_of_meetsUpperFace / …_of_meetsLowerFace — the window instances at the manuscript's geometry: V = (x+□_k) ∩ □_m meeting exactly one face of ∂□_m, extension to reflectedWindow x m k.

Where the face-vanishing hypothesis lives

The input is LocalizedZeroTraceFunctionOn (truncatedWindow x m k) (reflectedWindow x m k) v.toFun — CoarseGraining's own localized zero-trace predicate, with the reflected window as localization window. A cutoff supported there is compactly supported away from ∂(reflectedWindow), hence away from every unmet face of the window; only the met faces (interior to the reflected window) are constrained. This is the "face-only zero-trace glue", stated without a trace operator. It is a caller-supplied conditional API obligation: the supplier is the boundary-branch datum reduction (v − ℓ_h − v₁ vanishes on the met faces), not this module.

1. Integrability helpers

2. The weak gradient of the odd extension

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakGradientOn_oddFaceExtend_of_localizedZeroTrace {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUopen : IsOpen U) {i : Fin d} {a σ : ℝ} (hUsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ U ↔ y ∈ U) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (faceHalf U i a σ))] (v : HCPolySupport.H1Function (faceHalf U i a σ)) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (faceHalf U i a σ) U v.toFun) : HCPolySupport.HasWeakGradientOn U (oddFaceExtend a i (zeroExtend (faceHalf U i a σ) v.toFun)) (oddFaceExtendGrad a i (zeroExtendGrad (faceHalf U i a σ) v.grad))

The odd extension is H¹ across the interface, from face-only zero trace. U is open and invariant under the reflection r in {yᵢ = a}; v ∈ H¹(faceHalf U i a σ) has localized zero trace with localization window U. Then the odd extension of the zero extension of v has the reflected weak gradient on all of U.

3. The packaged H¹ function

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_h1Function_oddFaceExtend {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {i : Fin d} {a σ : ℝ} (hUsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ U ↔ y ∈ U) (v : HCPolySupport.H1Function (faceHalf U i a σ)) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (faceHalf U i a σ) U v.toFun) : ∃ (w : HCPolySupport.H1Function U), (∀ (y : HCPolySupport.Vec d), w.toFun y = oddFaceExtend a i (zeroExtend (faceHalf U i a σ) v.toFun) y) ∧ ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad a i (zeroExtendGrad (faceHalf U i a σ) v.grad) y

** A, abstract form.** The odd extension of a face-vanishing H¹ function of the half is an H¹ function of the whole reflection-symmetric domain, with toFun and grad pinned pointwise to the odd extension pair — verbatim the hwval (at c₀ = 0) and hwgrad slots of the proved consumers.

4. The stage-to-stage zero-trace transport

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_oddFaceExtend {d : ℕ} {H B V₀ : Set (HCPolySupport.Vec d)} (hHmeas : MeasurableSet H) (hBopen : IsOpen B) (hHB : H ⊆ B) {i : Fin d} {a : ℝ} (hBsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ B ↔ y ∈ B) (hVsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.coordFaceReflection a i y ∈ V₀ ↔ y ∈ V₀) {f : HCPolySupport.Vec d → ℝ} (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn H V₀ f) : HCPolySupport.LocalizedZeroTraceFunctionOn B V₀ (oddFaceExtend a i (zeroExtend H f))

The odd extension inherits face-only zero trace on the larger box. H ⊆ B are the consecutive boxes of the fold, B invariant under the reflection being unfolded, and V₀ (the common localization window of the whole chain) is invariant as well. A cutoff η supported in V₀ splits the extension as η·W = zeroExtend H (η·f) − (zeroExtend H ((η∘r)·f)) ∘ r, and the three H¹₀ closure facts of the core module do the rest.

5. The window instances (one met face)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h1FunctionOfSetEq_toFun {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (h : U = V) (u : HCPolySupport.H1Function U) : (h1FunctionOfSetEq h u).toFun = u.toFun

Transport of the value representative along an equality of H¹ domains.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_h1_oddFaceReflection_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m k j ∧ ¬MeetsLowerFace x m k j) (v : HCPolySupport.H1Function (truncatedWindow x m k)) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (truncatedWindow x m k) (reflectedWindow x m k) v.toFun) : ∃ (w : HCPolySupport.H1Function (reflectedWindow x m k)), (∀ (y : HCPolySupport.Vec d), w.toFun y = oddFaceExtend (1 / 2 * 3 ^ m) i (zeroExtend (truncatedWindow x m k) v.toFun) y) ∧ ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad (1 / 2 * 3 ^ m) i (zeroExtendGrad (truncatedWindow x m k) v.grad) y

** A on the windows, upper met face.** V = (x+□_k) ∩ □_m meets exactly the upper i-face of ∂□_m; a face-vanishing v ∈ H¹(V) produces the H¹ datum of the reflected window with toFun/grad pinned pointwise to the odd extension pair — the exact hwval (c₀ = 0) and hwgrad slots the boundary branch's odd producer asks for, and the hw slot of OddReflectionAssembly.isWeaklyHarmonicOn_reflectedWindow_of_meetsUpperFace.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_h1_oddFaceReflection_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m k j ∧ ¬MeetsLowerFace x m k j) (v : HCPolySupport.H1Function (truncatedWindow x m k)) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (truncatedWindow x m k) (reflectedWindow x m k) v.toFun) : ∃ (w : HCPolySupport.H1Function (reflectedWindow x m k)), (∀ (y : HCPolySupport.Vec d), w.toFun y = oddFaceExtend (-(1 / 2) * 3 ^ m) i (zeroExtend (truncatedWindow x m k) v.toFun) y) ∧ ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad (-(1 / 2) * 3 ^ m) i (zeroExtendGrad (truncatedWindow x m k) v.grad) y

** A on the windows, lower met face.**