SealOddGlue #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The flush-cube odd-harmonic comparator: the (W)(iv) glue #
What is proved #
The boundary lane's flush scale-n sub-cube K' = x' + □_n (x' = flushSubCentre z m n i σ) is a one-met-face truncated window: its σeᵢ
face lies exactly in the frontier of □_m and no other face of ∂□_m is met.
For a weakly Δ-harmonic v : H¹(K') whose value decomposes as v = w₀ + ρᵤ − ρₕ with w₀ ∈ H¹₀(□_m) (the anchor's own zero-trace witness) and ρᵤ, ρₕ ∈ H¹₀(K') (the two comparator correctors), this module produces — through the
proved OneStepOddPackaging/OddReflectionAssembly/Weyl chain — a globally
pointwise-odd, classically harmonic representative W on the doubled cube,
agreeing with v almost everywhere on K'
(exists_oddHarmonic_of_flushComparator), and composes it with the proved
flush-cube mean bound (A) into
|⨍_{K'} v| ≤ C(d) · ‖v − (v)_{K'}‖_{L²(K')}
No trace operator occurs.
The pointwise-odd upgrade #
Weyl's representative V agrees with the odd extension only almost everywhere.
V is continuous on the doubled window (harmonic functions are), the odd
extension is pointwise odd, and the doubled window is open and
reflection-symmetric, so V ∘ r = −V everywhere on it
(MeasureTheory.Measure.eqOn_open_of_ae_eq). The symmetrization
W := (V − V ∘ r)/2 is then globally pointwise odd, equals V on the doubled
window (hence is classically harmonic there and inherits the a.e.
identification), and is square-integrable.
References #
- ABK26,
l.harmonic.approximation.good.scales, Step 2.
1. The flush sub-cube is a one-met-face window #
The clamp proves inside the closed centre band.
Off the flush direction, the flush sub-cube meets no face of ∂□_m.
The met face, upper branch (σ = 1).
The met face, lower branch (σ = −1).
2. The descent geometry: the reflected window truncates back to K' #
The reflected window returns to the flush sub-cube inside □_m.
reflectedWindow x' m n ∩ □_m ⊆ (x' + □_n) ∩ □_m = K': the doubling happened
across the frontier face, so intersecting with the domain undoes it. This is
what lets the anchor's global H¹₀(□_m) witness descend through the reflected
window as localization window.
The doubled cube sits inside the reflected window.
3. The localized zero trace of the comparator difference #
The face-only zero trace, discharged.
The comparator difference v = w₀ + ρᵤ − ρₕ has localized zero trace on the
flush sub-cube through the reflected window: the anchor's H¹₀(□_m) witness
descends by reflectedWindow ∩ □_m ⊆ K', and the two H¹₀(K') correctors
localize through anything.
4. The odd harmonic representative on the doubled window #
The pointwise-odd classical representative, upper met face.
From a weakly Δ-harmonic v on a one-met-face truncated window with
face-only localized zero trace, a globally pointwise-odd W, square-integrable
on any D ⊆ reflectedWindow, classically harmonic on toEuc '' D, agreeing
with v almost everywhere on the window.
The pointwise-odd classical representative, lower met face.
The (W)(iv) glue at the flush sub-cube.
The two branch lemmas, entered from the flush geometry, with the localized zero trace discharged from the three-witness decomposition.
5. The flush-cube mean bound, applied to the comparator difference #
(A) discharged at the comparator difference.
The mean of the weakly Δ-harmonic comparator difference over the flush
sub-cube is priced by its own oscillation, at a d-only constant.