QuquartState
plain-language theorem explainer
The QuquartState abbreviation supplies the carrier space for the local quarter-turn core in coupled recognition models. Workers on Weyl relations and local operators in the Recognition framework cite this finite-dimensional complex vector space when defining basis kets and monomials. The definition is a one-line abbreviation of the function type Fin 4 → ℂ.
Claim. The ququart carrier space is the vector space of all functions from a four-element set to the complex numbers: $Q := (Fin 4 → ℂ)$.
background
In the CoupledRecognitionCores module the local quarter-turn core is modeled as a ququart carrier. The abbreviation imports the definition QuquartState := Fin 4 → ℂ from the parent module. This space serves as the domain for the standard basis ket |m⟩ and for the shift and phase operators that realize the Weyl algebra on four states.
proof idea
Direct abbreviation that re-exports the function space Fin 4 → ℂ as the ququart state type in the OperatorCore context. No further construction is performed.
why it matters
This carrier definition underpins the construction of the canonical shift operator X and phase operator Z on the ququart, which satisfy the Weyl relation ZX = i XZ. It is referenced by seven downstream declarations including basisKet, localWeylMonomial, and ququartWeyl_relation_apply. The definition fills the role of the single-core state space in the Recognition Science treatment of coupled cores.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.