liftOperator_intertwines
plain-language theorem explainer
The intertwining relation shows that lifting a linear operator T on a d-dimensional space to the coupled ququart core space preserves the action on embedded vectors exactly: lift(T) applied to embed(v) equals embed(T v). Researchers constructing finite-dimensional dynamics inside larger recognition-core Hilbert spaces cite this result. The proof is a direct unfolding of the lift definition followed by simplification via the projection-embedding cancellation lemma.
Claim. Let $d, N$ be natural numbers with $d ≤ 4^N$. For any linear map $T: ℂ^d → ℂ^d$ and vector $v ∈ ℂ^d$, the lifted operator satisfies lift(T)(embed(v)) = embed(T v), where embed zero-pads the vector into the space of $N$ coupled ququarts via the index equivalence and lift composes projection, $T$, and re-embedding.
background
CoupledCoreIndex N is the configuration space Fin N → Fin 4, indexing the Hilbert space of N coupled ququart cores. embedState zero-pads a d-dimensional vector into this space by mapping indices through coupledCoreEquivFin and setting excess components to zero. liftOperator is the composition embedState ∘ T ∘ projectState, which lifts T by projecting to the d-dimensional subspace, applying T, and embedding the result back. The upstream theorem projectState_embedState states that projection after embedding recovers the original vector exactly.
proof idea
The proof unfolds the definition of liftOperator to expose the composition embedState ∘ T ∘ projectState applied to embedState v. It then invokes projectState_embedState to cancel the inner projectState and embedState pair, reducing directly to embedState (T v). This is a one-line wrapper relying on the projection-embedding identity.
why it matters
This result feeds the finite_dimensional_exact_embedding theorem, which shows any finite-dimensional linear dynamics embeds exactly into a coupled-core carrier with N = d (using d ≤ 4^d). It ensures the embedding construction is faithful for operators, supporting exact realization of finite-dimensional models inside the ququart-based space. In the Recognition Science setting this closes the interface between abstract linear dynamics and the concrete coupled-core carriers derived from the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.