finite_dimensional_exact_embedding
plain-language theorem explainer
Any linear operator on a d-dimensional complex vector space embeds exactly into the coupled-core Hilbert space of dimension 4^d via zero-padding. Researchers modeling recognition-based quantum dynamics would cite this to justify using ququart carriers for arbitrary finite systems. The proof constructs the lift explicitly from embedState and projectState, then invokes the intertwining property to confirm exact action on embedded vectors.
Claim. Let $d$ be a natural number and $T$ a linear operator on the $d$-dimensional space of functions from Fin $d$ to $ℂ$. There exists a linear operator $L$ on the space of functions from (Fin $d$ → Fin 4) to $ℂ$ such that $L$ applied to the zero-padded embedding of any vector $v$ equals the zero-padded embedding of $T v$.
background
CoupledCoreSpace $N$ is the Hilbert space of functions from CoupledCoreIndex $N$ to $ℂ$, where CoupledCoreIndex $N$ consists of all maps Fin $N$ → Fin 4 and therefore has cardinality exactly $4^N$ by the cardinality theorem. The embedState map zero-pads a $d$-dimensional vector into this larger space whenever $d ≤ 4^N$; the liftOperator is then defined by composing embedState, the original operator, and the corresponding projection. This construction sits inside the CoupledRecognitionCores module, which assembles concrete carriers for coupled recognition cores built from ququart sites.
proof idea
The tactic proof first obtains the capacity bound $d ≤ 4^d$ by simplifying self_le_four_pow_self against coupledCoreIndex_card. It then refines the existential to the concrete liftOperator applied to this bound and the given $T$. The required intertwining equality on embedded vectors is discharged directly by the lemma liftOperator_intertwines.
why it matters
The result establishes exact compatibility between arbitrary finite-dimensional linear dynamics and the ququart-based coupled-core carriers used throughout the Recognition Science monolith. It supplies the embedding step needed to realize standard quantum operators inside the recognition framework without approximation or truncation. No downstream theorems are recorded yet, but the declaration closes a basic interface between conventional linear algebra and the core model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.