liftOperator
plain-language theorem explainer
The liftOperator definition constructs a linear operator on the coupled-core Hilbert space from a smaller operator T on a d-dimensional space by composing the zero-padding embedding, T itself, and the projection back. Researchers extending finite-dimensional linear dynamics into larger ququart-core carriers would cite this when building exact embeddings. The definition is realized as a direct composition of the three maps using linear-map composition.
Claim. Let $d,N$ be natural numbers with $d$ at most the cardinality of the index set of $N$ coupled ququart cores. For any linear map $T$ from the $d$-dimensional complex vector space to itself, the lifted operator on the space of complex functions on the index set is the composition of the embedding map (zero-padding into the larger space), $T$, and the projection map (extracting the first $d$ components).
background
CoupledCoreIndex N is the finite configuration space Fin N → Fin 4 whose cardinality is exactly 4^N. CoupledCoreSpace N is the associated Hilbert space of all complex-valued functions on this index set. The embedState map (defined upstream) zero-pads a vector in Fin d → ℂ into this larger space by placing its components in the initial slots according to the coupledCoreEquivFin ordering and setting the remainder to zero. The projectState map performs the complementary extraction of those initial components. The module develops the linear algebra of these coupled recognition cores as carriers for finite-dimensional dynamics.
proof idea
This is a one-line definition that applies the linear-map composition operation to embedState h, the operator T, and projectState h.
why it matters
The definition supplies the operator lift used by the downstream theorem liftOperator_intertwines, which establishes exact reproduction of T on the embedded subspace, and by finite_dimensional_exact_embedding, which guarantees that any finite-dimensional linear dynamics embeds exactly into a coupled-core carrier of sufficient capacity. Within the Recognition Science foundation this supplies the concrete mechanism for lifting operators while preserving action on the embedded subspace, supporting the construction of exact finite-dimensional embeddings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.