NegationSymmetry

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

(J3) negation symmetry of the clause-(i) slot families

ABK26, Section 4.1.

N : CutoffSample d → CutoffSample d ,     N ω = −ω  (every shell negated)

acts on the clause-(i) data in exactly two ways: it is the identity on every shell-norm-built slot, and it is the transpose on every coefficient-built slot. Cutoff.negateCutoffSample is the proved carrier map. The matching measure-preservation statement Cutoff.map_negateCutoffSample_cutoffSampleLaw (the descent of the frozen ShellLawJ3.negation through the lower-tail subtype) is also proved, but it is not consumed: every invariance below is a pointwise identity, so the transposed estimate is obtained sample by sample rather than in law. Nothing new is assumed anywhere in this file.

This module collects the pointwise N-invariances that the transposed ugly estimate needs:

• the three shell gauges shellW1InfGradNorm, shellW2InfNormAt and the localCubeControl block (norms are even);
• the four even slot families annularGradBlock, annularL2Block, gradTailSq, shellW2InfLatticeMax;
• the good event 𝒢₁(m; s, T) — every one of its two clauses is a shell-norm functional;
• the good event 𝒢₀(m) and the hlam datum — the λ_{γ,2} atoms, which are not norm-built but are transpose invariant because the skew part drops out of the coarse quadratic form (proved as CoarseEllipticity.lambdaSq_adjointFamily, transported to the sample by Localization.lambdaSq_negateCutoffSample).

The 𝓔_{s,2,2} atom is handled separately in TransposeError.lean.

References

• ABK26; (𝒢₀); (𝒢₁).

Part A -- the shell gauges are even

theorem Algsuperdiff.Section4.Provider.Annular.shellW1InfGradNorm_negate {d : ℕ} (m : ℤ) (j : Frozen.Assumptions.ShellField d) : Support.shellW1InfGradNorm m j.negate = Support.shellW1InfGradNorm m j

The W^{1,∞} shell gauge is even: it is a maximum of two norms.

theorem Algsuperdiff.Section4.Provider.Annular.shellW2InfNormAt_negate {d : ℕ} (z : HCPolySupport.Vec d) (k : ℤ) (j : Frozen.Assumptions.ShellField d) : Support.shellW2InfNormAt z k j.negate = Support.shellW2InfNormAt z k j

The W^{2,∞} shell gauge at a translated cube is even.

Part B -- the four even slot families

theorem Algsuperdiff.Section4.Provider.Annular.annularGradBlock_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : annularGradBlock M m (Section3.Cutoff.negateCutoffSample omega) j n = annularGradBlock M m omega j n

The 𝒢₁-derived gradient block is N-invariant.

theorem Algsuperdiff.Section4.Provider.Annular.annularL2Block_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : annularL2Block M m (Section3.Cutoff.negateCutoffSample omega) j n = annularL2Block M m omega j n

The 𝒢₁-derived L² block is N-invariant.

theorem Algsuperdiff.Section4.Provider.Annular.gradTailSq_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : gradTailSq M m (Section3.Cutoff.negateCutoffSample omega) = gradTailSq M m omega

The squared ℓ¹ shell tail is N-invariant.

Part C -- the good event 𝒢₁ is N-invariant

theorem Algsuperdiff.Section4.Provider.Annular.mem_eventG1_negateCutoffSample_iff {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s T : ℝ) (omega : Section3.Cutoff.CutoffSample d) : Section3.Cutoff.negateCutoffSample omega ∈ Support.eventG1 M m s T ↔ omega ∈ Support.eventG1 M m s T

𝒢₁(m; s, T) is invariant under whole-sequence negation, pointwise: both printed clauses are functionals of the shell gauges alone.

Part D -- the λ atoms and the good event 𝒢₀

theorem Algsuperdiff.Section4.Provider.Annular.cutoffLowerEllipticityInvLiteral_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (domainScale cutoffScale : ℤ) (s : ℝ) (q : Section3.CoarseEllipticityExponent) (omega : Section3.Cutoff.CutoffSample d) : Section3.Observable.cutoffLowerEllipticityInvLiteral M domainScale cutoffScale s q (Section3.Cutoff.negateCutoffSample omega) = Section3.Observable.cutoffLowerEllipticityInvLiteral M domainScale cutoffScale s q omega

The literal centered inverse lower multiscale ellipticity is N-invariant.

The skew part of the coefficient drops out of the coarse quadratic form, so λ_{s,q}(Q; aᵀ) = λ_{s,q}(Q; a) (CoarseEllipticity.lambdaSq_adjointFamily); combined with the (J3) carrier identity a_m(−ω) = a_m(ω)ᵀ this is exactly Localization.lambdaSq_negateCutoffSample.

theorem Algsuperdiff.Section4.Provider.Annular.mem_eventG0_negateCutoffSample_iff {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : Section3.Cutoff.negateCutoffSample omega ∈ Support.eventG0 M Ccg m ↔ omega ∈ Support.eventG0 M Ccg m

𝒢₀(m) is invariant under whole-sequence negation, pointwise.