QuquartState
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not equip the space with an inner product or norm.
- Does not enforce normalization or unitarity of states.
- Does not link the carrier to the J-cost function or phi-ladder.
- Does not impose any periodicity or modular arithmetic beyond the Fin 4 domain.
formal statement (Lean)
12abbrev QuquartState := Fin 4 → ℂ
proof body
Definition body.
13
14/-- The standard basis ket `|m⟩`. -/