TransposeDischarge #

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

The transposed ugly estimate, discharged by the `(J3)` symmetry #

ABK26, Section 4.1, p.mathcalE.annular.decomp: the manuscript runs e.ugly.estimate.for.J a second time for the transposed field and asserts the same right-hand side.

This module formalizes exactly that argument. Write N ω = −ω for the proved negation of the whole shell sequence on the genuine lower-tail carrier (Cutoff.negateCutoffSample). Then:

a_L(Nω) = a_L(ω)ᵀ — the proved (J3) carrier identity Cutoff.coefficientCutoff_negateCutoffSample_eq_adjoint, itself a consequence of the proved skewness of the genuine lower-infinite cutoff;
the flux-correction constant (k_L − k_m)_{□_m} is linear in the shell fields, so it changes sign under N (fluxIncrementAverage_negateCutoffSample), and therefore ã_{L,m}(Nω) = ã_{L,m}(ω)ᵀ pointwise (fluxCorrectedField_negateCutoffSample);
every shell-norm-built slot is literally N-invariant, and the two variational slots (λ_{γ,2} and 𝓔_{s,2,2}) are N-invariant because the skew part drops out of the coarse quadratic form (NegationSymmetry.lean, TransposeError.lean);
consequently the transposed J-leg at ω is the field J-leg at Nω (jLegField_negateCutoffSample), and the ugly estimate for the transposed field at ω is the proved field-side ugly estimate (exists_uglyJEstimate_annulus_of_eventG1) evaluated at Nω.

The ugly estimate itself is never re-proved: it is transported. And the transport is deterministic — the ruled "same law" is not consumed. Every step above is a pointwise identity on the carrier, so the transposed estimate holds at each individual sample, not merely in law; the proved Cutoff.map_negateCutoffSample_cutoffSampleLaw is not used. The only almost-sure input is the atom-versus-representative reconciliation annularErrorAtomMax_ae_le_annularErrorLatticeMax, which the field-side leg already consumes at the same place.

The payoff #

The transposed ugly estimate is thereby available at every sample, with the transposed response family no longer a free variable: it is the concrete fun ω L ↦ annularResponseMax M L m (N ω). A consumer of it is therefore a transcription of the field-side leg, not a substitution. Because the atom-versus-representative reconciliation is only almost sure, the transposed estimate has to be produced inside the filter_upwards of the display, exactly where the field-side estimate already is.

References #

ABK26, (ã_{L,m}), (the transposed ugly estimate).

Part A -- the flux-corrected field transposes under `N` #

source

theorem Algsuperdiff.Section4.Provider.Annular.fluxIncrementAverage_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (Q : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) :

Support.fluxIncrementAverage M L m Q (Section3.Cutoff.negateCutoffSample omega) = -Support.fluxIncrementAverage M L m Q omega

The cube-averaged flux increment changes sign under N. It is linear in the shell fields; equivalently, it is the transpose of itself at ω, and it is antisymmetric.

source

theorem Algsuperdiff.Section4.Provider.Annular.fluxCorrectedField_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (Q : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) :

Support.fluxCorrectedField M L m Q (Section3.Cutoff.negateCutoffSample omega) x = HCPolySupport.matTranspose (Support.fluxCorrectedField M L m Q omega x)

The flux-corrected coefficient transposes under N, pointwise: ã_{L,m}(Nω)(x) = ã_{L,m}(ω)(x)ᵀ. The a_L leg transposes by the (J3) carrier identity and the subtracted antisymmetric constant changes sign, which is exactly what the transpose of the difference demands.

source