OneStepBoundaryEndpoint

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

The boundary-branch excess-decay endpoint

OneStepSchauderChain.excessDecay_oneStep_interior_of_harmonicApprox closed the four Schauder slots of OneStepConditional.excessDecay_oneStep_of_harmonicApprox on the interior branch, at K_h = 0. This module does the same on the boundary branch, through the boundary branch's split Schauder bound:

  Csch = boundarySchauderConst d = 48 · 3^{3/2} · schauderConst d · √((24(d+1))^d) ,
  K_h  = boundarySchauderConst d · (3^{-n})^{1/2} · (3^{-(n-2)} · boundaryDatumLeg …) .

The competitor enters through classical harmonicity on the doubled window reflectedWindow x m (n-2) — which is what OneStepSchauderComposeBoundary.exists_classicalCompetitor_reflectedWindow produces from a variationally harmonic odd extension — together with its square-integrability there. Nothing here restricts the met set: the geometry of OneStepBoundaryGeometry is uniform in it.

What is still open, precisely

1. The _of_weaklyHarmonic level. OneStepSchauderComposeInterior.excessDecay_oneStep_interior_of_weaklyHarmonic removes the classical-harmonicity slot by applying Weyl's lemma on the anchor's moved replacement cube y + □_{n-2}, which is exactly where the anchor's hharm lives. On the boundary branch the Schauder competitor lives on reflectedWindow x m (n-2), and the moved replacement cube is not contained in it (in a met coordinate the clamped cube protrudes on the window side: windowLo ≥ y_i − ½·3^{n-2}), so the two representatives must be identified on U_2 — where both are continuous and both agree a.e. with the competitor — before hharm can be transported. That identification, plus the EqOn transfer of gradField and of affineExcess, is the remaining assembly; it is bookkeeping, not analysis.

1. Square integrability against affine competitors on the doubled window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integrableOn_sub_affineEval_sq_reflectedWindow {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (reflectedWindow x m k))) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => (u p - Support.affineEval c g p) ^ 2) (reflectedWindow x m k) MeasureTheory.volume