ShellLawJ3

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

structure Algsuperdiff.Frozen.Assumptions.ShellLawJ3 (d : ℕ) (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) : Prop

ABK26 (J3): the joint law of the entire shell sequence is invariant under every hyperoctahedral conjugation and, separately, under whole-sequence negation.

• hyperoctahedral (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R) : P.map (ShellField.rotateSequence R hR) = P
• negation : P.map ShellField.negateSequence = P