OneStepPartialReflection

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

The multi-face odd reflection, unconditional

The iteration

exists_h1_oddReflection_chain runs the Finset induction over the met set. At each stage B_T → B_{T∪{i}} it invokes

• the packaging (OneStepOddPackaging.exists_h1Function_oddFaceExtend) at the proved stage geometry (faceHalf_partialReflectedWindow_insert_*, mem_partialReflectedWindow_coordFaceReflection_iff_*),
• the zero-trace transport (OneStepOddPackaging.localizedZeroTraceFunctionOn_oddFaceExtend),

carrying four invariants: weak harmonicity on B_T; the restriction pinning (w = v pointwise on the window); pointwise oddness under every already unfolded met-face reflection; and the face-only zero trace of the stage function, localized in the full box B_S. The oddness invariant is exact (no null sets): the newly unfolded face is odd by the very shape of oddFaceExtend, and the previously unfolded faces stay odd because distinct coordinate reflections commute and each stage box is invariant under them.

The endpoint

exists_h1_oddReflection_reflectedWindow: for any met configuration (interior, one face, edge, corner), a weakly harmonic v ∈ H¹((x+□_k) ∩ □_m) with face-only zero trace has a weakly harmonic H¹ extension to reflectedWindow x m k that restricts to v on the window and is pointwise odd under every met-face reflection. The met set is realized as the Finset.filter of the met-face predicates (metSet), so the one-face hypothesis hother of the proved transfer is gone.

The operator reconciliation (the extension is a fixed point of the proved partial odd reflection oddExtend, a.e.) and the composition into the proved Schauder consumers are in OneStepPartialReflectionCompose.

1. Distinct coordinate reflections commute

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coordFaceReflection_comm {d : ℕ} {i j : Fin d} (hij : i ≠ j) (a b : ℝ) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection a i (HCPolySupport.coordFaceReflection b j y) = HCPolySupport.coordFaceReflection b j (HCPolySupport.coordFaceReflection a i y)

Face reflections in distinct coordinates commute, for arbitrary pivots.

2. Monotonicity of the intermediate boxes

theorem Algsuperdiff.Section4.Provider.ExcessDecay.partialReflectedWindow_subset_of_subset {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) {T T' : Finset (Fin d)} (hTT' : T ⊆ T') : partialReflectedWindow x m k T ⊆ partialReflectedWindow x m k T'

The intermediate boxes grow with the reflected set: reflecting more faces only enlarges the box. Proved pointwise (the endpoint comparisons fail for degenerate windows, exactly as in truncatedWindow_subset_reflectedWindow).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_subset_partialReflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (T : Finset (Fin d)) : truncatedWindow x m k ⊆ partialReflectedWindow x m k T

The window sits inside every intermediate box.

3. The met set

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.metSet {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : Finset (Fin d)

The met set of the window (x+□_k) ∩ □_m: the coordinates whose upper or lower face of ∂□_m is met. Classical choice supplies the decidability of the two real inequalities.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_metSet_iff {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} : i ∈ metSet x m k ↔ MeetsUpperFace x m k i ∨ MeetsLowerFace x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.partialReflectedWindow_metSet {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : partialReflectedWindow x m k (metSet x m k) = reflectedWindow x m k

At the met set, the last intermediate box is the fully reflected window.

4. The chain: the per-stage packaging, constructed

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_h1_oddReflection_chain {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {S : Finset (Fin d)} (hSup : ∀ i ∈ S, MeetsUpperFace x m k i ∨ MeetsLowerFace x m k i) (v : HCPolySupport.H1Function (truncatedWindow x m k)) (hv : Support.IsWeaklyHarmonicOn (truncatedWindow x m k) v) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (truncatedWindow x m k) (partialReflectedWindow x m k S) v.toFun) (T : Finset (Fin d)) : T ⊆ S → ∃ (w : HCPolySupport.H1Function (partialReflectedWindow x m k T)), Support.IsWeaklyHarmonicOn (partialReflectedWindow x m k T) w ∧ (∀ y ∈ truncatedWindow x m k, w.toFun y = v.toFun y) ∧ (∀ j ∈ T, (MeetsUpperFace x m k j → ∀ (z : HCPolySupport.Vec d), w.toFun (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) j z) = -w.toFun z) ∧ (MeetsLowerFace x m k j → ∀ (z : HCPolySupport.Vec d), w.toFun (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) j z) = -w.toFun z)) ∧ HCPolySupport.LocalizedZeroTraceFunctionOn (partialReflectedWindow x m k T) (partialReflectedWindow x m k S) w.toFun

The multi-face chain, unconditional. From a weakly harmonic v ∈ H¹((x+□_k) ∩ □_m) with face-only zero trace (localized in B_S), every intermediate box B_T, T ⊆ S, carries a weakly harmonic H¹ function that restricts to v on the window, is pointwise odd under every unfolded met-face reflection, and again has face-only zero trace localized in B_S.

5. The endpoint: the reflected window, any met configuration

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_h1_oddReflection_reflectedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) (v : HCPolySupport.H1Function (truncatedWindow x m k)) (hv : Support.IsWeaklyHarmonicOn (truncatedWindow x m k) v) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (truncatedWindow x m k) (reflectedWindow x m k) v.toFun) : ∃ (w : HCPolySupport.H1Function (reflectedWindow x m k)), Support.IsWeaklyHarmonicOn (reflectedWindow x m k) w ∧ (∀ y ∈ truncatedWindow x m k, w.toFun y = v.toFun y) ∧ ∀ (i : Fin d), (MeetsUpperFace x m k i → ∀ (z : HCPolySupport.Vec d), w.toFun (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -w.toFun z) ∧ (MeetsLowerFace x m k i → ∀ (z : HCPolySupport.Vec d), w.toFun (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z) = -w.toFun z)

** B at the H¹ level.** For any met configuration of the window (x+□_k) ∩ □_m — interior, one face, edge or corner — a weakly harmonic v ∈ H¹ with face-only zero trace extends to a weakly harmonic H¹(reflectedWindow x m k) function that restricts to v on the window and is pointwise odd under every met-face reflection. The one-met-face hypothesis of the proved transfer is gone.