QuquartState
QuquartState supplies the four-dimensional complex vector space that carries a single local quarter-turn core. It is referenced by every subsequent definition of basis vectors, shift and phase operators, and Weyl monomials inside the CoupledRecognitionCores module. The declaration is a direct one-line alias to the upstream abbrev, inheriting its type without additional proof steps.
claimLet $Q$ denote the vector space of all functions from the set of four elements to the complex numbers, written $Q := (Fin 4) → ℂ$.
background
The CoupledRecognitionCores module treats the local quarter-turn core as a ququart carrier whose state space is the type Fin 4 → ℂ. This type is imported from the Foundation layer and re-aliased at the OperatorCore level to serve as the common domain for all local linear operators. The upstream doc-comment states that the local quarter-turn core is modeled as a ququart carrier, fixing the finite-dimensional setting before any operator or inner-product structure is added.
proof idea
The declaration is a one-line wrapper that aliases the upstream definition QuquartState := Fin 4 → ℂ from CoupledRecognitionCores.
why it matters in Recognition Science
QuquartState is the carrier type for the entire local operator algebra, appearing in the definitions of basisKet, ququartX, ququartZ, localWeylMonomial, and the Weyl relation lemma. These constructions feed the coupled-core index and tensor monomials that realize the Recognition Composition Law at the quarter-turn scale. The alias closes the import boundary between Foundation and OperatorCore layers, allowing the eight-tick octave structure to be expressed on a single core before spatial dimension D = 3 is recovered at higher levels.
scope and limits
- Does not equip the space with an inner product or norm.
- Does not define any linear operators or basis vectors.
- Does not impose normalization or phase conventions on the functions.
formal statement (Lean)
9abbrev QuquartState := IndisputableMonolith.Foundation.CoupledRecognitionCores.QuquartState