OneStepCornerSeam

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

The boundary gradient-Hölder producer at every met configuration

The single boundary producer of the §4.3 one-step chain: for a competitor odd about every met face of the doubled window, classically harmonic there, the gradient-Hölder seminorm on U₃ is bounded by the interior display

  [∇V]_{C^{0,1/2}(U₃)} ≤ C(d) (3^{-n})^{1/2} E(V, U₂)

with no boundary-datum leg, at every met configuration: one met face upper or lower, and every corner/edge orientation.

The three inputs it composes

• the orientation-free corner pricing (★★) (OneStepCornerTransport.exists_oddClassDefect_le_affineExcessRaw_corner_any) and the two one-met-face pricings (★) (OneStepEvenBoundFinal's upper face, OneStepCornerTransportFace's lower face);
• the a.e. seam of OneStepCornerSeamCore: the oddness binder here is the pointwise-on-the-window one, which is what a Weyl representative satisfies (its a.e. oddness upgrades by continuity), while (★)/(★★) want the global pointwise binder. The piecewise representative W = V on the doubled window, = 0 off it, is globally odd about every met face, and every quantity the pricing reads is an a.e. invariant, so the pricing transfers back to V;
• the almost-everywhere odd bridge OneStepBoundaryOdd.exists_gradientHolder_boundary_odd_ae, run at O := W.

1. The fold arithmetic

2. The producer

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_gradientHolder_boundary_metSet (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (i : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → MeetsUpperFace x m (n - 2) i ∨ MeetsLowerFace x m (n - 2) i → (∀ (l : Fin d), MeetsUpperFace x m (n - 2) l → ∀ y ∈ reflectedWindow x m (n - 2), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l y) = -V y) → (∀ (l : Fin d), MeetsLowerFace x m (n - 2) l → ∀ y ∈ reflectedWindow x m (n - 2), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l y) = -V y) → InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2)) → MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))) → Support.IsAffineMinimizer (truncatedWindow x m (n - 2)) V (c - HCPolySupport.vecDot A x) A → ∃ (K : ℝ), 0 ≤ K ∧ (∀ (l : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => gradField V p l) (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 ≤ C * (3 ^ (-n)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m (n - 2)) V

The boundary producer at every met configuration, from window-pointwise oddness: one leg.

The met set is arbitrary but nonempty; the oddness binders are read on the doubled window, which is what the chain's Weyl representative satisfies. The odd-class defect has been folded into the excess leg by (★) / (★★).