ququartWeyl_relation
plain-language theorem explainer
The alias supplies the ququart Weyl commutation relation ZX = i XZ for direct reference in the OperatorCore layer. Researchers constructing four-level quantum models or coupled operator algebras in Recognition Science cite it to fix the phase factor in the Weyl algebra. It is realized as a one-line alias to the imported theorem.
Claim. Let $X$ and $Z$ be the ququart operators on the four-dimensional state space. Then $Z X = i X Z$.
background
QuquartState is the four-dimensional complex Hilbert space equipped with basis vectors via basisKet. The operators ququartX and ququartZ are the standard generators satisfying the Weyl algebra on this space. The module CoupledRecognitionCores defines these operators together with their compositions; the present alias imports the relation into the OperatorCore namespace for use in tensor constructions.
proof idea
The declaration is a one-line alias to the theorem ququartWeyl_relation in CoupledRecognitionCores. That theorem is proved by applying LinearMap.ext to obtain pointwise equality on states, followed by direct invocation of ququartWeyl_relation_apply.
why it matters
The relation supplies the canonical phase factor for ququart operator products and is referenced by tensorWeylMonomial and localWeylMonomial. It anchors the algebraic structure of coupled recognition cores. In the Recognition framework it fixes the commutation rule required for consistent operator monomials at the foundation level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.