ququartX
plain-language theorem explainer
The ququartX definition supplies the canonical shift operator on the four-dimensional ququart state space. Researchers constructing discrete quantum models or the Recognition Science eight-tick structure would cite it when building Weyl relations or basis transformations. The definition is realized as a linear map that applies the prev4 index shift to the state function, with linearity following from pointwise simplification.
Claim. The shift operator $X$ on the ququart state space $H = (Z/4Z to C)$ is the linear map defined by $(X psi)(m) = psi(m-1 mod 4)$ for all $m in Z/4Z$.
background
In the CoupledRecognitionCores module the ququart state is the carrier abbrev QuquartState := Fin 4 to C, representing the local quarter-turn core. The sibling def prev4 computes the predecessor index modulo 4 via (m.val + 3) % 4, which realizes the convention that X maps basis ket |m> to |m+1 mod 4>. This sits inside the Recognition Science treatment of the eight-tick octave, drawing on the upstream EightTick.phase that supplies phases k pi /4 for k = 0 to 7.
proof idea
One-line wrapper that applies prev4 to the function argument. Additivity is shown by introducing two states, extending pointwise, and simplifying with the definition of prev4; scalar multiplication follows identically by the same pointwise reduction.
why it matters
This operator feeds the downstream ququartWeyl_relation theorem (ZX = i XZ) and the basis-action theorem ququartX_basisKet. It supplies the shift generator required by the eight-tick octave (T7) inside the coupled-recognition cores, enabling the discrete Weyl algebra that precedes the emergence of D = 3 spatial dimensions (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.