ququartZ_basisKet
plain-language theorem explainer
The theorem establishes that the phase operator Z multiplies each standard basis ket |m⟩ by the factor i raised to the power m. Workers on discrete quantum models or Recognition Science operator algebras cite this when checking diagonal action before deriving Weyl relations. The proof works by extending the state equality to each index and splitting on whether the index matches m, then simplifying with the definitions of the ket and the phase map.
Claim. For each $m$ in the four-element index set, the phase operator $Z$ satisfies $Z |m⟩ = i^m |m⟩$, where $|m⟩$ is the standard basis vector that equals 1 at position $m$ and 0 elsewhere.
background
The standard basis ket |m⟩ is the function on the four indices that returns 1 precisely when the argument equals m and 0 otherwise. The phase operator Z is the linear map that multiplies the m-th component of any state vector ψ by i^m. These objects live in the CoupledRecognitionCores module, which supplies the basic operator algebra for four-level systems used throughout the Recognition Science foundation.
proof idea
The proof extends the functional equality to an arbitrary index n. It then performs case analysis on whether n equals m. When the indices match, both sides reduce to i^m by direct substitution into the definitions of the basis ket and the phase map. When they differ, both sides are zero.
why it matters
The result supplies the diagonal action needed to verify the pointwise Weyl relation ZX ψ = i XZ ψ that follows immediately in the same module. It therefore anchors the operator algebra for ququart states before any further Recognition Science constructions that rely on these four-level degrees of freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.