OneStepOddMultiFace

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

The multi-met-face harmonicity transfer

This module builds them and proves the iteration.

The boxes

partialReflectedWindow x m k T is the coordinate box whose i-edge is the reflected edge for i ∈ T and the window edge otherwise. It is again an open bounded convex box (all three properties are per-coordinate), it is truncatedWindow at T = ∅, and it is reflectedWindow as soon as T contains every met coordinate.

The step

The two geometric facts of OddReflectionAssembly hold verbatim at a general B_T, and without the single-met-face hypothesis: the tangential coordinates of B_{T ∪ {i}} and B_T agree by construction, so the one-face computation is the only one that happens.

• mem_partialReflectedWindow_coordFaceReflection_iff_upper — B_T is invariant under the reflection in a met face i ∈ T (its reflected i-edge has endpoints summing to 3^m);
• faceHalf_partialReflectedWindow_insert_upper — the half of B_{T ∪ {i}} on the window side of the met i-face is B_T.

Composing them with HarmonicityTransferFace.isWeaklyHarmonicOn_of_oddFaceExtendGrad gives the single step isWeaklyHarmonicOn_partialReflectedWindow_insert_upper and its lower-face twin: one met face is unfolded at a time, at any stage of the fold.

The iteration

isWeaklyHarmonicOn_partialReflectedWindow_of_chain runs the induction over the met set: given a family of H¹ data, one per intermediate box, each pinned to the odd extension of the previous one's gradient, weak harmonicity propagates from B_∅ to every B_T with T inside the met set — and hence, by partialReflectedWindow_eq_reflectedWindow, to the fully reflected window (isWeaklyHarmonicOn_reflectedWindow_of_chain). As in the one-face case the H¹ packaging at each stage is an input, not an output.

Scope note (measured, not hidden)

What is removed here is the one-met-face restriction on the transfer. The odd affine class still collapses at two met faces (OddReflectionMap.affineLift_eq_zero_of_two_met: at an edge or corner of □_m the only odd affine function is 0), so the odd-class pricing of the boundary datum degenerates in the corner regime — that is a property of the class, not of this transfer.

1. The intermediate partially reflected boxes

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

The lower endpoint of the i-edge of the box that reflects exactly the faces of T.

Equations

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

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

The upper endpoint of the i-edge of the box that reflects exactly the faces of T.

Equations

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

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

The intermediate box B_T: the window with exactly the faces of T reflected.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_partialReflectedWindow_iff {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {T : Finset (Fin d)} {y : HCPolySupport.Vec d} : y ∈ partialReflectedWindow x m k T ↔ ∀ (i : Fin d), partialReflectedLo x m k T i < y i ∧ y i < partialReflectedHi x m k T i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.partialReflectedLo_insert_of_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {T : Finset (Fin d)} {i j : Fin d} (hji : j ≠ i) : partialReflectedLo x m k (insert i T) j = partialReflectedLo x m k T j

theorem Algsuperdiff.Section4.Provider.ExcessDecay.partialReflectedHi_insert_of_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {T : Finset (Fin d)} {i j : Fin d} (hji : j ≠ i) : partialReflectedHi x m k (insert i T) j = partialReflectedHi x m k T j

theorem Algsuperdiff.Section4.Provider.ExcessDecay.partialReflectedWindow_empty {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : partialReflectedWindow x m k ∅ = truncatedWindow x m k

At T = ∅ the intermediate box is the window itself.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.partialReflectedWindow_eq_reflectedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {S : Finset (Fin d)} (hS : ∀ i ∉ S, ¬MeetsUpperFace x m k i ∧ ¬MeetsLowerFace x m k i) : partialReflectedWindow x m k S = reflectedWindow x m k

As soon as T contains every met coordinate, the intermediate box is the fully reflected window.

2. The intermediate boxes are open bounded convex domains

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.convex_partialReflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (T : Finset (Fin d)) : Convex ℝ (partialReflectedWindow x m k T)

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

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

3. The two geometric facts at a general intermediate box

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_partialReflectedWindow_coordFaceReflection_iff_upper {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) {T : Finset (Fin d)} (hiT : i ∈ T) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i y ∈ partialReflectedWindow x m k T ↔ y ∈ partialReflectedWindow x m k T

Reflection invariance at an already unfolded met upper face.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_partialReflectedWindow_coordFaceReflection_iff_lower {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) {T : Finset (Fin d)} (hiT : i ∈ T) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i y ∈ partialReflectedWindow x m k T ↔ y ∈ partialReflectedWindow x m k T

Reflection invariance at an already unfolded met lower face.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf_partialReflectedWindow_insert_upper {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) {T : Finset (Fin d)} (hiT : i ∉ T) : faceHalf (partialReflectedWindow x m k (insert i T)) i (1 / 2 * 3 ^ m) 1 = partialReflectedWindow x m k T

The previous box is the half of the next one, upper met face. No single-met-face hypothesis: the tangential edges agree by construction.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.faceHalf_partialReflectedWindow_insert_lower {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) {T : Finset (Fin d)} (hiT : i ∉ T) : faceHalf (partialReflectedWindow x m k (insert i T)) i (-(1 / 2) * 3 ^ m) (-1) = partialReflectedWindow x m k T

The previous box is the half of the next one, lower met face.

4. The single unfolding step, at any stage

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_partialReflectedWindow_insert_upper {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) {T : Finset (Fin d)} (hiT : i ∉ T) (v : HCPolySupport.H1Function (partialReflectedWindow x m k T)) (hv : Support.IsWeaklyHarmonicOn (partialReflectedWindow x m k T) v) (w : HCPolySupport.H1Function (partialReflectedWindow x m k (insert i T))) (hw : ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad (1 / 2 * 3 ^ m) i (zeroExtendGrad (partialReflectedWindow x m k T) v.grad) y) : Support.IsWeaklyHarmonicOn (partialReflectedWindow x m k (insert i T)) w

One met upper face unfolded, at any stage of the fold.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isWeaklyHarmonicOn_partialReflectedWindow_insert_lower {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) {T : Finset (Fin d)} (hiT : i ∉ T) (v : HCPolySupport.H1Function (partialReflectedWindow x m k T)) (hv : Support.IsWeaklyHarmonicOn (partialReflectedWindow x m k T) v) (w : HCPolySupport.H1Function (partialReflectedWindow x m k (insert i T))) (hw : ∀ (y : HCPolySupport.Vec d), w.grad y = oddFaceExtendGrad (-(1 / 2) * 3 ^ m) i (zeroExtendGrad (partialReflectedWindow x m k T) v.grad) y) : Support.IsWeaklyHarmonicOn (partialReflectedWindow x m k (insert i T)) w

One met lower face unfolded, at any stage of the fold.

5. The iteration