embedState
plain-language theorem explainer
The embedState definition constructs a linear map that zero-pads any d-dimensional complex vector into the Hilbert space of N coupled ququart cores whenever d does not exceed 4^N. Researchers embedding finite-dimensional quantum dynamics into the Recognition Science core framework cite this map to lift states and operators exactly. The definition enumerates configurations via coupledCoreEquivFin, places input components in the initial segment of the ordered basis, and returns zero elsewhere, with linearity verified by case splitting and simp.
Claim. Let $d, N$ be natural numbers with $d ≤ 4^N$. The linear map $ι : ℂ^d → ℂ^{(ℤ/4ℤ)^N}$ is defined by $ι(v)(s) = v_i$ when the enumerated index $i$ of configuration $s$ satisfies $i < d$, and $ι(v)(s) = 0$ otherwise.
background
CoupledCoreIndex N is the configuration space Fin N → Fin 4 of N ququart cores. CoupledCoreSpace N is the Hilbert space of all complex functions on this index set and therefore has dimension exactly 4^N. The auxiliary map coupledCoreEquivFin supplies the bijection from CoupledCoreIndex N onto Fin (4^N) that orders the basis.
proof idea
The definition gives an explicit formula: for input vector v and configuration s, compute finite index i via coupledCoreEquivFin N s; return the corresponding entry of v if i < d and zero otherwise. Preservation of addition and scalar multiplication is shown by extensionality, splitting on the if-condition, and simplification.
why it matters
This embedding is invoked by embedState_injective, finite_dimensional_exact_embedding, liftOperator, and liftOperator_intertwines. It supplies the concrete mechanism for realizing any finite-dimensional linear operator exactly inside a coupled-core carrier of sufficient size. In the Recognition framework the construction therefore lets arbitrary finite-dimensional dynamics sit inside the discrete 4^N-dimensional space of coupled cores.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.