OneStepOddValue

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

The value-level odd pinning of the boundary competitor

OneStepBoundaryOdd runs the boundary branch through the odd class under the pointwise everywhere hypothesis oddExtend x m k V = V on the competitor. The proved one-met-face transfer (OddReflectionAssembly.isWeaklyHarmonicOn_reflectedWindow_of_meets{Upper,Lower}Face) pins only the gradient of the reflected H¹ datum, and Weyl's lemma (OneStepSchauderComposeBoundary.exists_classicalCompetitor_reflectedWindow) returns a classical competitor only up to a null set. This module closes that interface gap.

Three observations

• Oddness is a reflection identity, not a fold identity. In the one-met-face regime the fold windowFold acts only in the met coordinate, where it is the identity on the window side and the face reflection coordFaceReflection a i beyond it, with the matching sign. Hence any O with O ∘ coordFaceReflection a i = -O satisfies oddExtend x m k O = O off the interface hyperplane {yᵢ = a} — no membership hypothesis at all (oddExtend_eq_self_of_faceOdd_upper). The interface is Lebesgue-null, so the identity holds almost everywhere.

• Almost-everywhere suffices. normalizedL2On is an integral, so it is an almost-everywhere invariant (normalizedL2On_congr_ae); the odd bridge therefore runs verbatim from oddExtend x m k O =ᵐ O and V =ᵐ O + c₀.

• The additive constant is free. The gradient pinning determines the value of the reflected H¹ datum only up to an additive constant (two H¹ functions with the same weak gradient on a connected open set differ by a constant), and a constant is not in the odd class. It does not have to be: a constant is an admissible affine competitor, so the whole chain runs with V =ᵐ O + c₀ and the odd affine datum read at the shifted intercept c - c₀. Taking c₀ = 0 recovers OneStepBoundaryOdd verbatim.

What is delivered

affineExcessRaw_reflectedWindow_le_odd_ae and exists_gradientHolder_boundary_odd_ae — the almost-everywhere twins's odd bridge and boundary producer — together with the pointwise atom oddExtend_eq_self_of_faceOdd_upper and its lower-face twin, and the face-oddness of the one-face odd extension oddFaceExtend (which is exactly the value-level shape of the object whose gradient the proved transfer pins).

1. normalizedL2On is an almost-everywhere invariant

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_congr_ae {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (h : f =ᵐ[MeasureTheory.volume.restrict W] g) : Support.normalizedL2On W f = Support.normalizedL2On W g

The volume-normalized L² seminorm only sees the almost-everywhere class of its argument: it is a set integral. No measurability and no finiteness of the window is needed.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.affineDistOn_eq_normalizedL2On {d : ℕ} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d → ℝ) (c : ℝ) (g : HCPolySupport.Vec d) : Support.affineDistOn W u c g = Support.normalizedL2On W fun (y : HCPolySupport.Vec d) => u y - Support.affineEval c g y

The affine distance, unfolded to the seminorm of the affine residual.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.affineDistOn_congr_ae {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (h : f =ᵐ[MeasureTheory.volume.restrict W] g) (c : ℝ) (A : HCPolySupport.Vec d) : Support.affineDistOn W f c A = Support.affineDistOn W g c A

The affine distance is an almost-everywhere invariant.

2. Face oddness implies the fold identity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddExtend_eq_self_of_faceOdd_upper {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {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) {O : HCPolySupport.Vec d → ℝ} (hO : ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -O z) {y : HCPolySupport.Vec d} (hne : y i ≠ 1 / 2 * 3 ^ m) : oddExtend x m k O y = O y

The interface atom, upper face. In the one-met-face regime the partial odd extension oddExtend fixes every function which is odd about the met face, off the interface hyperplane. The met face supplies the fold in its own coordinate; the unmet coordinates are untouched.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddExtend_ae_eq_self_of_faceOdd_upper {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {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) {O : HCPolySupport.Vec d → ℝ} (hO : ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -O z) : oddExtend x m k O =ᵐ[MeasureTheory.volume] O

The interface is null. The pointwise atom therefore holds almost everywhere, upper face.

3. The odd bridge, almost everywhere

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.affineExcessRaw_reflectedWindow_le_odd_ae {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hkm : k < m) {V O : HCPolySupport.Vec d → ℝ} {c₀ : ℝ} (hVO : V =ᵐ[MeasureTheory.volume.restrict (reflectedWindow x m k)] fun (y : HCPolySupport.Vec d) => O y + c₀) (hOodd : oddExtend x m k O =ᵐ[MeasureTheory.volume.restrict (reflectedWindow x m k)] O) {c : ℝ} {A : HCPolySupport.Vec d} (hodd : IsOddAffineData x m k (c - c₀) A) (hRpos : 0 < (MeasureTheory.volume (reflectedWindow x m k)).toReal) (hUpos : 0 < (MeasureTheory.volume (truncatedWindow x m k)).toReal) (hOR : MeasureTheory.MemLp O 2 (MeasureTheory.volume.restrict (reflectedWindow x m k))) : Support.affineExcessRaw (reflectedWindow x m k) V ≤ 2 ^ d * Support.affineDistOn (truncatedWindow x m k) V (c - HCPolySupport.vecDot A x) A

The odd bridge, almost-everywhere form. For a competitor which agrees almost everywhere on the doubled window with O + c₀, where O is fixed by the partial odd extension almost everywhere, and an affine datum whose shifted intercept c - c₀ lies in the odd class, the excess minimum on the doubled window is at most 2^d times the affine distance on U₂.

With c₀ = 0 and a pointwise-odd V this is the pointwise odd-class excess bound on the doubled window.

4. The boundary producer, almost everywhere

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_gradientHolder_boundary_odd_ae {d : ℕ} [NeZero d] (hd : d ≠ 0) {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hmn : n - 2 < m) {V O : HCPolySupport.Vec d → ℝ} {c₀ : ℝ} (hVO : V =ᵐ[MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))] fun (y : HCPolySupport.Vec d) => O y + c₀) (hOodd : oddExtend x m (n - 2) O =ᵐ[MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))] O) {c : ℝ} {A : HCPolySupport.Vec d} (hodd : IsOddAffineData x m (n - 2) (c - c₀) A) (hharm : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2))) (hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2)))) : ∃ (K : ℝ), 0 ≤ K ∧ (∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => gradField V p i) (truncatedWindow x m (n - 3)) MeasureTheory.volume) ∧ Support.HasGradientOn (truncatedWindow x m (n - 3)) V (gradField V) ∧ Support.HolderSeminormBoundOn (truncatedWindow x m (n - 3)) (1 / 2) K (gradField V) ∧ K ≤ boundaryOddSchauderConst d * (3 ^ (-n)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m (n - 2)) V + boundaryOddSchauderConst d * (3 ^ (-n)) ^ (1 / 2) * (3 ^ (-(n - 2)) * oddClassDefect x m n V c A)

The Schauder gradient-Hölder estimate, boundary branch — the producer from an almost-everywhere odd competitor.

The almost-everywhere twin of the pointwise odd-class producer: the competitor is only required to agree almost everywhere on the doubled window with O + c₀ for an almost-everywhere odd O, which is exactly what Weyl's lemma delivers off the reflected H¹ datum.