coupledBasisKet
plain-language theorem explainer
This definition supplies the standard basis vector in the Hilbert space of N coupled ququart cores, indexed by a configuration s. Researchers building orthonormal bases or tensor-Weyl operators in coupled recognition models cite it directly. The body is a direct indicator function returning 1 at the matching index and 0 elsewhere.
Claim. For a configuration $s$ in the space of $N$-site assignments to four states, the vector $|s⟩$ in $ℂ^{4^N}$ with component at $t$ equal to 1 if $t=s$ and 0 otherwise.
background
The coupled-core index space is the set of all functions from a finite set of $N$ sites to four states, representing configurations of coupled ququart cores. The associated Hilbert carrier is the set of all complex-valued functions on this index space, with dimension exactly $4^N$. This construction appears in the foundation layer for building operators on recognition cores, as referenced in the upstream definitions of the index space and the function space to complex numbers.
proof idea
The definition is implemented directly as a function that evaluates to 1 when the input index matches the parameter $s$ and to 0 otherwise. No lemmas are applied; it is a primitive indicator construction on the finite index set.
why it matters
This basis vector serves as the foundation for downstream results such as the orthonormality theorem for the coupled standard basis and the Hilbert-Schmidt-style pairing on coupled-core operators. It supports the tensor-Weyl monomial constructions that map basis states to phased shifted states, aligning with the ququart state space in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.