embedState_injective
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove surjectivity onto the full carrier space.
- Does not apply when d exceeds the core cardinality.
- Does not address infinite-dimensional or continuous limits.
- Does not incorporate time evolution or dynamical equations.
formal statement (Lean)
568theorem embedState_injective {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N)) :
569 Function.Injective (embedState h) := by
proof body
Term-mode proof.
570 intro v w hEq
571 have hproj := congrArg (projectState h) hEq
572 simpa [projectState_embedState] using hproj
573
574/-- Lift a finite-dimensional linear operator to the coupled-core carrier by
575zero-padding, acting, and projecting back. -/