ququartWeyl_relation
plain-language theorem explainer
The ququart Weyl relation states that the phase operator Z and shift operator X on the four-dimensional ququart state space satisfy ZX = i XZ. Researchers modeling discrete quantum systems or Recognition Science foundations would cite this for operator algebra consistency in coupled cores. The proof reduces the operator equality to pointwise verification by applying LinearMap.ext and invoking the supporting lemma ququartWeyl_relation_apply.
Claim. Let $Z$ and $X$ be the phase and shift operators on the ququart state space. Then $Z X = i X Z$.
background
QuquartState is the finite-site configuration space of coupled ququart cores. The shift operator X acts by X ψ(m) = ψ(prev4 m), cycling through the four basis states. The phase operator Z acts by Z ψ(m) = i^m ψ(m). Their composition uses the standard linear map composition. The supporting lemma ququartWeyl_relation_apply establishes the relation pointwise: Z(X ψ) = i X(Z ψ) by finite case analysis on the index m.
proof idea
The proof is a one-line wrapper that applies LinearMap.ext to reduce operator equality to pointwise action on an arbitrary state ψ, then invokes the lemma ququartWeyl_relation_apply which verifies the identity by fin_cases on m followed by simp.
why it matters
This theorem supplies the canonical Weyl commutation relation for ququart operators inside the coupled recognition cores module. It feeds the reexported abbrev in OperatorCore.CoupledRecognitionCores and supports discrete quantum modeling aligned with the Recognition Science forcing chain steps T5 through T7. No open scaffolding remains for this specific relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.