prev4
plain-language theorem explainer
The definition supplies the modular predecessor on Fin 4 that implements the cyclic shift convention for the ququart X operator. Researchers constructing discrete Weyl operators or verifying commutation relations on four-level systems cite it when building basis transformations. It is realized by a direct arithmetic construction that adds 3 and reduces modulo 4, with the omega tactic discharging the Fin bound.
Claim. For each $m$ in the cyclic group of order 4, define the predecessor index by $prev_4(m) := (m + 3) mod 4$. This shift satisfies the operator convention $X|m⟩ = |m+1 mod 4⟩$.
background
In the CoupledRecognitionCores module, QuquartState denotes the type of complex-valued functions on Fin 4, representing states of a four-level quantum system. The standard basis vectors are supplied by basisKet m, which equals 1 at index m and 0 elsewhere. The definition prev4 provides the index map used to define the linear operator ququartX, which pulls values from the predecessor index and thereby realizes a cyclic permutation on the basis.
proof idea
This is a direct definition that constructs the Fin 4 element as the pair consisting of (m.val + 3) % 4 together with the omega tactic to confirm the result lies in the required range 0 to 3.
why it matters
The definition is invoked inside ququartX to define the canonical shift operator, inside ququartX_basisKet to establish the action on basis kets, and inside ququartWeyl_relation_apply to prove the pointwise Weyl relation ZX = i XZ. It supplies the period-4 generator required for the discrete operator algebra in the Recognition Science foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.