OneStepDatumZeroTrace

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

The hzt supplier: face-only zero trace of the datum-split competitor

  hzt : LocalizedZeroTraceFunctionOn (truncatedWindow x m (n-2))
          (reflectedWindow x m (n-2)) v.toFun

for the manuscript's odd competitor V_odd = v − ℓ_h − v₁ (: "v − ℓ_h − v₁ vanishes on the met portion of ∂□_m"). This module produces that hypothesis from the chain's own binders — no new caller-supplied mathematical proposition:

• u − h ∈ H¹₀(□_m) — the Dirichlet datum of the frozen theorem (IsDirichletSolutionOn's HasZeroTraceDifferenceOn component);
• v₁ − Ψ ∈ H¹₀(U₂) with Ψ = h − ℓ_h on U₂ — the datum corrector's own output (OneStepDatumSplit.exists_datumCorrector composed with the clamp's match and the H¹ realization of h − ℓ_h).

The decomposition

  v − ℓ − v₁ = (v − u) + (u − h) + (h − ℓ − Ψ) + (Ψ − v₁) ,

and each summand has the localized zero trace:

1. v − u and Ψ − v₁ are H¹₀(U₂) — any cutoff product stays in H¹₀(U₂) (CoarseGraining's localizedZeroTraceFunctionOn_of_h10_any).
2. h − ℓ − Ψ vanishes pointwise on U₂, so every cutoff product vanishes on U₂ and is trivially H¹₀(U₂) (memH10_of_forall_eq_zero).
3. u − h is H¹₀(□_m), and a cutoff supported in the reflected window localizes it into H¹₀(U₂): the product's H¹₀(□_m) approximants are supported in tsupport η ∩ □_m ⊆ reflectedWindow ∩ □_m = U₂ (memH10_mul_of_tsupport_subset + the geometric identity reflectedWindow_inter_openCubeSet). This is where "zero trace on the met face only" is genuinely spent: the reflected window crosses ∂□_m exactly through the met faces, so the localization keeps the datum identity u = h there and discards the rest of ∂□_m.

No trace operator, no max principle, no analytic input: the supplier is pure H¹₀ bookkeeping on the chain's structural binders. (The max-principle content of the datum reduction lives in OneStepDatumSplit, where v₁ is priced; here v₁ only needs its trace structure.)

References

• CoarseGraining Homogenization/Sobolev/H1/LocalizedZeroTrace.lean (the predicate), Homogenization/Sobolev/H1/Algebra/H10Function.lean (mulContDiffHasCompactSupport).

1. The reflected window meets the domain cube in the window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedWindow_inter_openCubeSet {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : reflectedWindow x m k ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) = truncatedWindow x m k

The reflected window crosses ∂□_m only through the met faces. Inside □_m the partial reflection adds nothing: coordinatewise, a met edge is extended only beyond the corresponding face of □_m, and an unmet edge is not moved at all.

2. H¹₀ localization by a cutoff

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memH10_mul_of_tsupport_subset {d : ℕ} {B V : Set (HCPolySupport.Vec d)} (hB : IsOpen B) (hV : IsOpen V) {f : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemH10 B f) {η : HCPolySupport.Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηV : tsupport η ⊆ V) : HCPolySupport.MemH10 (V ∩ B) fun (y : HCPolySupport.Vec d) => η y * f y

Cutoff localization of H¹₀. If f ∈ H¹₀(B) and η is a smooth compactly supported cutoff with tsupport η ⊆ V, then η·f ∈ H¹₀(V ∩ B): the H¹₀(B) approximants of the product are supported in tsupport η ∩ tsupport (approx) ⊆ V ∩ B, and every field of the witness restricts.

3. Functions vanishing on the window are trivially H¹₀

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memH10_of_forall_eq_zero {d : ℕ} {Ω : Set (HCPolySupport.Vec d)} (hΩ : MeasurableSet Ω) {f : HCPolySupport.Vec d → ℝ} (hf : ∀ y ∈ Ω, f y = 0) : HCPolySupport.MemH10 Ω f

A function vanishing pointwise on Ω is H¹₀(Ω). CoarseGraining's MemH10 constrains its witness only on Ω, so the zero approximation sequence serves.

4. Localized zero-trace producers

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_of_memH10 {d : ℕ} {Ω V : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemH10 Ω f) : HCPolySupport.LocalizedZeroTraceFunctionOn Ω V f

Any H¹₀(Ω) function has the localized zero trace, in any window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_of_forall_eq_zero {d : ℕ} {Ω V : Set (HCPolySupport.Vec d)} (hΩ : MeasurableSet Ω) {f : HCPolySupport.Vec d → ℝ} (hf : ∀ y ∈ Ω, f y = 0) : HCPolySupport.LocalizedZeroTraceFunctionOn Ω V f

A function vanishing pointwise on Ω has the localized zero trace, in any window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_truncatedWindow_of_memH10_cube {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) {f : HCPolySupport.Vec d → ℝ} (hf : HCPolySupport.MemH10 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) f) : HCPolySupport.LocalizedZeroTraceFunctionOn (truncatedWindow x m k) (reflectedWindow x m k) f

The cube-datum localization. A function of H¹₀(□_m) has the face-only localized zero trace on every truncated window, against the reflected window: a cutoff supported in reflectedWindow x m k localizes the global zero trace to reflectedWindow ∩ □_m = (x+□_k) ∩ □_m.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_congr {d : ℕ} {Ω V : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hfg : ∀ (y : HCPolySupport.Vec d), f y = g y) (hf : HCPolySupport.LocalizedZeroTraceFunctionOn Ω V f) : HCPolySupport.LocalizedZeroTraceFunctionOn Ω V g

Localized zero trace is invariant under pointwise-equal functions.