Symmetry #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Symmetries of the genuine lower-infinite cutoff #
This module begins the descent of the manuscript's sequence-level (J3) symmetries to the genuine lower-tail carrier. In particular, negation preserves the actual convergence carrier and turns the skew cutoff into its negative. No law-level symmetry is postulated here: the remaining measure transport must be derived from the exact whole-sequence J3 equality.
The literal shell scaling conjugates translation by z to translation by
3^{-k} z before scaling.
J1 stationarity of shell zero, transported through the exact marginal scaling law, gives real-translation stationarity of every shell marginal.
The canonical law of the whole shell sequence is invariant under every real translation. This is derived from the independent coordinates, their exact marginal scaling, and J1; it is not a new model field.
The exact deterministic local cutoff control is unchanged by shell negation.
The lower-tail carrier is stable under every real spatial translation. The new enclosing origin scale is deterministic in the requested scale and translation; it does not depend on the shell or on a realization.
Real translation restricted to the genuine lower-tail carrier.
Equations
Instances For
Translation on the lower-tail carrier is measurable.
J1 stationarity descends from the whole canonical sequence law to the actual lower-tail carrier law, for every real translation.
The lower-tail convergence condition is closed under simultaneous whole-sequence negation.
Whole-sequence negation restricted to the genuine public cutoff carrier.
Equations
Instances For
Whole-sequence negation is a genuine involution on the lower-tail carrier.
The negation action on the lower-tail carrier is measurable.
J3 negation invariance descends from the whole shell-sequence law to the actual lower-tail carrier law.
Translating the input sequence translates the genuine lower-infinite cutoff, as an exact identity of regular coefficient fields.
The actual coefficient cutoff commutes exactly with every real translation.
The coefficient-cutoff law is invariant under every real translation. CoarseGraining's stationary-law interface is its integer-translation specialization.
The exact CoarseGraining carrier-level stationarity predicate for the coefficient cutoff law.
The lower-tail carrier is stable under every signed-permutation conjugation. The deterministic polynomial comparison is only used to retain summability; no probabilistic symmetry is assumed here.
Signed-permutation conjugation restricted to the genuine lower-tail carrier.
Equations
- Algsuperdiff.Section3.Cutoff.rotateCutoffSample R hR omega = ⟨Algsuperdiff.Frozen.Assumptions.ShellField.rotateSequence R hR ↑omega, ⋯⟩
Instances For
Signed-permutation conjugation on the lower-tail carrier is measurable.
Conjugation by R.transpose is the right inverse of conjugation by R on
the genuine cutoff carrier.
The exact whole-sequence J3 hyperoctahedral equality descends to the genuine lower-tail carrier law.
Signed-permutation conjugation commutes exactly with the genuine lower-infinite
cutoff, in CoarseGraining's R.transpose * a(Rx) * R convention.
Signed-permutation conjugation commutes exactly with the actual
coefficient cutoff a_m = nu I + k_m.
The law of the actual coefficient cutoff has the exact CoarseGraining
signed-permutation isotropy required by IsIsotropicInLawR.
Negating the input sequence negates the genuine lower-infinite cutoff. This is an identity of regular coefficient fields, not an almost-everywhere representative statement.
Under whole-sequence negation, the actual coefficient cutoff becomes the adjoint coefficient cutoff. This uses the proved skewness of the genuine lower-infinite cutoff; it does not assume an adjoint law.
The law of the actual coefficient cutoff is invariant under adjunction.
This is the J3 negation symmetry transported through the genuine lower-tail
carrier and the exact identity a_m(-omega) = a_m(omega)^*.