embedState_injective
plain-language theorem explainer
The zero-padding embedding of a d-dimensional complex vector into the Hilbert space of N coupled ququart cores is injective whenever d is at most the cardinality of the core index set. Researchers constructing finite approximations to recognition states cite this to guarantee that distinct vectors remain distinguishable after lifting. The proof is a one-line term-mode wrapper that applies the left-inverse property of the projection map.
Claim. Let $H_N$ be the Hilbert space of $N$ coupled ququart cores with basis indexed by the set $I_N = (Fin N) → (Fin 4)$. For any $d ≤ |I_N|$, the zero-padding map $ι : ℂ^d → H_N$ is injective.
background
CoupledCoreIndex N is the type Fin N → Fin 4, the finite-site configuration space of coupled ququart cores. The map embedState h zero-pads a vector from Fin d → ℂ into the full carrier by placing its entries in the initial positions of the enumerated basis given by coupledCoreEquivFin. The companion map projectState h restricts any state in the full space back to its first d coordinates.
proof idea
The proof is a short term-mode argument. Assume embedState h v = embedState h w. Apply projectState h to both sides via congrArg. The round-trip identity projectState_embedState then reduces both sides to v and w, so v = w.
why it matters
This result secures faithful lifting of lower-dimensional states into the coupled-core carrier, a prerequisite for consistent operator constructions in the recognition framework. It supports the development of linear actions that preserve distinctions, consistent with the need for injective embeddings in the overall forcing chain. No downstream uses are recorded, so the lemma functions as a basic structural property for later coupled-system arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.