OneStepOddClassCornerFinal

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

The corner pricing (★★), assembled

's residue (2): at a window meeting two upper faces the odd affine class collapses to {0} (affineLift_eq_zero_of_two_met), and this module prices the resulting degenerate defect:

• exists_normalizedL2On_le_affineExcessRaw_corner — (★★): for V classically harmonic on the doubled window and odd under every met-face reflection, ‖V‖_{L²(U₂)} ≤ C(d)·E_raw(U₂,V).
• exists_oddClassDefect_le_affineExcessRaw_corner — the consumer shape: oddClassDefect x m n V 0 0 ≤ C(d)·E_raw(U₂,V) at the corner datum (0,0), the only member of the collapsed class.

The absorption

With ℓ* a minimizer, f = V − ℓ*, E = ‖f‖_{L²(U₂)}, P = ‖ℓ*‖_{L²(U₂)} and the split ℓ* = evenᵢ + evenⱼ − e_{ij}, the three applications of OneStepOddClassCornerApp give

  ‖evenᵢ‖, ‖evenⱼ‖ ≤ 3·Caff·Vr·E + Λt·(E+P) ,
  ‖e_{ij}‖ ≤ 3·Caff·Vr·E + Λt·(E+P) + 2·Λt·(P + ‖evenᵢ‖) ,

with Λ = Λ(d) collecting the Hessian, fold and ramp coefficients and the depth fraction t = min(1/16, 1/(8Λ)) making Λt ≤ 1/8. The linear program closes at P ≤ (104/11)·3·Caff·Vr·E + (13/11)·E, whence ‖V‖ ≤ E + P ≤ C(d)·E with C(d) = (104/11)·3·Caff·Vr + 24/11 explicit in d (through Caff, Vr and the transplanted interior Hessian constant).

Scope (disclosed)

Upper-upper met pairs, matching every proved one-face convention; the met set is otherwise arbitrary. Lower/mixed corners need the mechanical lower-face twins or a negation transport (not built here). The oddness binders are the global pointwise identities, as in the proved (★).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_normalizedL2On_le_affineExcessRaw_corner (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (i j : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → i ≠ j → MeetsUpperFace x m (n - 2) i → MeetsUpperFace x m (n - 2) j → (∀ (l : Fin d), MeetsUpperFace x m (n - 2) l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l z) = -V z) → (∀ (l : Fin d), MeetsLowerFace x m (n - 2) l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l z) = -V z) → 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 → Support.normalizedL2On (truncatedWindow x m (n - 2)) V ≤ C * Support.affineExcessRaw (truncatedWindow x m (n - 2)) V

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_oddClassDefect_le_affineExcessRaw_corner (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (i j : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → i ≠ j → MeetsUpperFace x m (n - 2) i → MeetsUpperFace x m (n - 2) j → (∀ (l : Fin d), MeetsUpperFace x m (n - 2) l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l z) = -V z) → (∀ (l : Fin d), MeetsLowerFace x m (n - 2) l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l z) = -V z) → 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 → oddClassDefect x m n V 0 0 ≤ C * Support.affineExcessRaw (truncatedWindow x m (n - 2)) V

The corner defect pricing —'s residue (2), the consumer shape. At the corner datum (0,0) (the only member of the collapsed odd class), the odd-class defect is priced by the excess itself.