ququartZ
plain-language theorem explainer
ququartZ defines the phase operator Z on the ququart state space of functions from Fin 4 to the complex numbers by pointwise multiplication with i to the power m. Researchers modeling discrete four-state systems or deriving Weyl commutation relations cite this operator when constructing finite-dimensional representations of phase and shift generators. The definition is supplied directly as a linear map, with additivity and homogeneity verified by simplification and ring tactics.
Claim. The phase operator $Z$ on the ququart space (functions $ψ : Fin 4 → ℂ$) acts by $(Zψ)(m) = i^m ψ(m)$ for each $m ∈ Fin 4$, where $i = √(-1)$.
background
QuquartState is the abbreviation for the vector space of all functions from the finite index set Fin 4 to the complex numbers, serving as the carrier for the local quarter-turn core. This models a four-level system whose discrete symmetry is generated by phase and shift operators. The upstream definition of QuquartState supplies the domain and codomain for the linear map; the operator is introduced to realize the canonical Z generator in this finite setting.
proof idea
The definition is given by the explicit pointwise rule toFun ψ m := Complex.I ^ m.val * ψ m. Linearity follows from two separate proofs: map_add' reduces to ring normalization after extensionality and simp, while map_smul' likewise simplifies by ring after extensionality.
why it matters
ququartZ supplies the phase factor required by the downstream theorems ququartWeyl_relation (ZX = i XZ) and ququartZ_basisKet (Z|m⟩ = i^m |m⟩). It therefore anchors the algebraic relations that realize the coupled recognition cores and feeds the discrete symmetry generators used in the foundation layer. Within the Recognition Science chain this operator supports the eight-tick octave by providing the Z element of the ququart algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.