ququartWeyl_relation_apply
plain-language theorem explainer
The lemma establishes the pointwise Weyl commutation relation on ququart states, showing that the phase operator Z applied after the cyclic shift X equals i times the reverse ordering. Researchers modeling finite-dimensional quantum systems or discrete operator algebras would cite it to confirm algebraic consistency in four-level carriers. The proof proceeds by exhaustive case analysis over the four indices, using simplification with the operator definitions and algebraic reduction via i squared equals negative one.
Claim. For any state vector $ψ : Fin 4 → ℂ$, $Z(Xψ) = i · X(Zψ)$, where $X$ is the cyclic shift with $(Xψ)(m) = ψ(m-1 mod 4)$ and $Z$ is the diagonal phase operator with $(Zψ)(m) = i^m ψ(m)$.
background
The module CoupledRecognitionCores models quarter-turn cores via ququart states. QuquartState is the type Fin 4 → ℂ, serving as the carrier for four-level discrete states. The shift operator ququartX is defined by (ququartX ψ) m = ψ (prev4 m), where prev4 computes the predecessor index modulo 4 to realize X|m⟩ = |m+1 mod 4⟩. The phase operator ququartZ multiplies componentwise by i to the power of the index, (ququartZ ψ) m = i^m · ψ m. Upstream definitions of prev4, ququartX, and ququartZ supply the concrete actions used throughout.
proof idea
The tactic proof applies extensionality to reduce the operator equality to pointwise checks on each index m. It then invokes fin_cases to split into four exhaustive cases. Simplification with ququartZ, ququartX, and prev4 disposes of the middle cases directly. The first and third cases require explicit ring calculations that invoke the identity i² = -1, obtained from Complex.I_sq and rewritten via sq.
why it matters
This lemma supplies the pointwise verification that feeds the parent theorem ququartWeyl_relation, which asserts the full operator equality ququartZ.comp ququartX = i • (ququartX.comp ququartZ). It closes a verification step inside the CoupledRecognitionCores module, supporting the algebraic structure of coupled recognition cores. The relation provides a discrete analog of Weyl commutation used in the foundation layer of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.