ququartZ
plain-language theorem explainer
The ququartZ abbreviation exports the canonical phase operator on the four-dimensional ququart state space. Workers on discrete Weyl algebras or coupled core models cite this when assembling the Z operator for phase multiplications. The construction is a direct linear map that scales each component ψ(m) by i raised to the index m.
Claim. The phase operator $Z$ on the ququart state space is the linear map defined by $(Zψ)(m) = i^m ψ(m)$ for each basis index $m ∈ {0,1,2,3}$.
background
The CoupledRecognitionCores module defines operators acting on QuquartState, the complex vector space of dimension four whose elements are functions from Fin 4 to ℂ. The ququartZ operator is the diagonal phase operator with entries given by successive powers of the imaginary unit. It is constructed to be linear, as verified by the map_add' property in its definition. This setup supports the introduction of Weyl relations between phase and shift operators on the same space.
proof idea
This declaration is a one-line wrapper that re-exports the phase operator definition from the core module IndisputableMonolith.Foundation.CoupledRecognitionCores.
why it matters
This definition supplies the Z operator required to establish the ququart Weyl relation ZX = i XZ and the explicit action Z|m⟩ = i^m |m⟩. It forms part of the algebraic foundation for coupled recognition cores, enabling discrete operator models that may connect to the self-similar structures in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.