projectState
plain-language theorem explainer
projectState defines the linear projection that restricts a state in the N-ququart coupled-core space to its first d coordinates via the canonical finite enumeration. Researchers modeling finite-dimensional approximations or operator lifts in recognition cores cite this when composing embeddings with projections. The definition supplies the pointwise action directly from the basis equivalence, with linearity holding by reflexivity on the function-space operations.
Claim. Let $d,N$ be natural numbers with $d$ at most the cardinality of the index set of $N$ coupled ququarts. The linear map from the space of functions on configurations (Fin $N$ to Fin 4) to complex $d$-tuples sends a state vector $ψ$ to the vector whose $i$-th entry is $ψ$ evaluated at the preimage under the enumeration bijection of the cast of $i$ into the full index set.
background
CoupledCoreIndex N is the set of all assignments of one of four levels to each of N sites, written Fin N → Fin 4. CoupledCoreSpace N is the complex vector space of all functions from this index set to ℂ, hence a Hilbert space of dimension exactly 4^N. The upstream enumeration coupledCoreEquivFin supplies the explicit bijection from this index set onto Fin (4^N), allowing any finite-dimensional subspace to be identified with the initial segment of the standard basis.
proof idea
The definition installs the toFun clause that composes the input function with the inverse of the enumeration and the castLE truncation. The two linearity axioms are discharged by reflexivity because addition and scalar multiplication act pointwise on the function space.
why it matters
The definition supplies the left inverse needed for the round-trip identity projectState_embedState and for the injectivity argument in embedState_injective. It is the projection half of the operator-lifting construction liftOperator, which embeds finite-dimensional linear maps into the full coupled-core carrier. Within the Recognition framework this supplies the concrete mechanism for dimensional reduction on ququart chains, consistent with the eight-tick octave and the phi-ladder truncation steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.