OneStepOddCompose #

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

Plumbing for the boundary producer: local identification and `EqOn` transfer #

OneStepOddValue runs the boundary branch's Schauder producer from an almost-everywhere odd competitor. This module supplies the two pieces of plumbing that producer needs once its datum is the variationally harmonic H¹ datum on the doubled window: the local identification of the two Weyl representatives, and the transfer of the representative's two consumers along the resulting EqOn.

The local identification device #

's eqOn_of_ae_eq_of_continuous needs global continuity, which no Weyl representative has: harmonicity is asserted only on the window. The local twin eqOn_of_ae_eq_of_continuousOn is the same proof with ContinuousOn in place of Continuous: on an open S the disagreement set is open, hence null implies empty. Continuity on the window comes from harmonicity for free (HarmonicAt carries ContDiffAt ℝ 2), which is continuousOn_of_harmonicOnNhd.

This settles the identification of the two Weyl representatives the boundary branch produces: the interior route applies Weyl's lemma on the anchor's moved replacement cube R_mov, the boundary route on the doubled window reflectedWindow, and neither set contains the other — but both contain U₂, both representatives are continuous there and both agree almost everywhere with the competitor, so they agree pointwise on U₂ (two continuous harmonic representatives agreeing a.e. agree pointwise). The two consumers of the representative then transfer: gradField because fderiv is local, and affineExcess because it is an integral over U₂ (affineExcess_congr_eqOn).