QuquartState
plain-language theorem explainer
QuquartState supplies the type of all functions from a four-element set to the complex numbers, acting as the state carrier for a single ququart in the coupled recognition model. Researchers constructing local Weyl operators or basis expansions in the Recognition Science foundation layer cite this definition directly. The declaration is a bare type abbreviation with no computational reduction or lemmas required.
Claim. Let $Q$ denote the set of all functions from the discrete index set $I_4 = {0,1,2,3}$ to the complex scalars $ℂ$. This space serves as the carrier for states of the local quarter-turn core.
background
The CoupledRecognitionCores module models each local quarter-turn core via a ququart carrier. QuquartState is introduced as the function type Fin 4 → ℂ, which is the standard 4-dimensional complex vector space equipped with the usual pointwise operations. This definition is re-exported from the OperatorCore submodule to maintain a single source of truth for the carrier across the foundation layer.
proof idea
The declaration is a direct type abbreviation with no proof body. It simply equates the name QuquartState to the function type Fin 4 → ℂ and carries no lemmas or tactics.
why it matters
QuquartState is the foundational type for seven downstream declarations, including basisKet (the standard ket |m⟩), ququartX (the shift operator), ququartZ (the phase operator), localWeylMonomial, and the Weyl relation lemma ququartWeyl_relation_apply. It supplies the concrete 4-level discrete carrier needed to realize the local recognition operations that feed into the broader forcing chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.