OneStepOddClassCornerProducer

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

The corner producer: one leg

The corner sibling of the one-met-face gradient-Hölder producer: at a window meeting two upper faces, the boundary gradient-Hölder producer has a single leg — the interior display at the boundary, with no boundary-datum contribution. The odd-class defect at the corner datum (0,0) (the only member of the collapsed class) is folded into the excess by the corner pricing (★★) of OneStepOddClassCornerFinal.

This is the exact consumer shape the K-package chain (OneStepConditional.excessDecay_oneStep_of_harmonicApprox through exists_gradientHolder_boundary_odd_ae) expects, so the corner regime now composes with the proved one-step contraction the same way the one-face regime does.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.isOddAffineData_zero {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : IsOddAffineData x m k 0 0

The zero datum belongs to the odd affine class at every met configuration.