basisKet
plain-language theorem explainer
The function assigning to each index m in Fin 4 the vector in the space of maps Fin 4 to complex numbers that equals 1 at m and 0 elsewhere supplies the standard basis for the ququart carrier. Researchers constructing local Weyl operators or Hilbert-Schmidt pairings in finite-dimensional models cite this definition when proving orthonormality and operator actions. The definition is realized by a direct indicator function on the finite index set with no auxiliary lemmas.
Claim. For each $m$ in the finite set of four elements, the vector $|m⟩$ is the map from the same set to the complex numbers satisfying $|m⟩(n) = 1$ if $n = m$ and $0$ otherwise.
background
QuquartState is defined as the type of all functions from Fin 4 to the complex numbers and serves as the carrier for the local quarter-turn core. The basisKet supplies the canonical vectors in this space. The module imports the operator core that re-exports the identical construction, allowing downstream statements about local operators to reference the same basis without redefinition.
proof idea
The definition is given directly by the indicator: the map n maps to 1 precisely when n equals the fixed m and to 0 otherwise. No lemmas or tactics are applied; the body is the explicit case distinction on the finite set.
why it matters
This definition anchors every subsequent result on the ququart basis inside CoupledRecognitionCores, including the orthonormality theorem, the definition of the local operator inner product, and the action of the local Weyl monomials. It feeds the proofs that each Weyl monomial has Hilbert-Schmidt norm squared equal to 4 and that distinct phase labels are orthogonal. In the Recognition Science setting it realizes the finite-dimensional representation of the quarter-turn dynamics that precedes the full forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.