projectState_embedState
The theorem shows that restricting a zero-padded d-dimensional complex vector back to its original coordinates recovers the vector exactly when d is at most the dimension of the N-ququart configuration space. Researchers constructing finite-dimensional subspaces inside coupled recognition core models would cite it to confirm that padding and projection act as inverses on the image. The proof is a direct term-mode verification that applies function extensionality followed by unfolding and simplification via the basis enumeration equivalence.
claimLet $C_N$ be the Hilbert space of states for $N$ coupled ququart cores (dimension $4^N$). For $d ≤ 4^N$, let $ι: ℂ^d → C_N$ be the linear embedding that places the components of $v$ into the first $d$ positions of the enumerated basis and pads the remainder with zeros. Let $π: C_N → ℂ^d$ be the linear projection that extracts those first $d$ coordinates. Then $π(ι(v)) = v$ for every $v ∈ ℂ^d$.
background
CoupledCoreIndex N is the finite configuration space Fin N → Fin 4 that indexes the states of N coupled ququart recognition cores. The auxiliary equivalence coupledCoreEquivFin supplies a bijection from this space onto Fin(4^N), which is used to order the basis. embedState takes a vector in Fin d → ℂ and produces a linear map on the full space by assigning its entries to the initial segment of the enumerated basis and setting the rest to zero. projectState takes a full-space vector and returns the restriction to the first d enumerated coordinates via the inverse equivalence.
proof idea
The proof proceeds by function extensionality on the finite index set. It unfolds the definitions of projectState and embedState, then simplifies directly with the properties of coupledCoreEquivFin. This shows that the value recovered at each index i is exactly the original component of v, because the embedding places those components precisely in the positions selected by the projection.
why it matters in Recognition Science
The result is invoked in embedState_injective to deduce injectivity of the padding map and in liftOperator_intertwines to verify that lifted operators act correctly on the embedded subspace. It supplies the algebraic inverse relation needed for consistent finite-dimensional approximations inside the coupled-core Hilbert space. Within the Recognition Science framework this supports the treatment of finite-site configurations that appear in the forcing chain from T0 to the emergence of spatial dimension D=3.
scope and limits
- Does not treat the case d > 4^N.
- Does not establish norm preservation or unitarity of the embedding.
- Does not extend to infinite N or continuous limits.
- Does not address nonlinear maps on the state space.
formal statement (Lean)
560theorem projectState_embedState {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N))
561 (v : Fin d → ℂ) :
562 projectState h (embedState h v) = v := by
proof body
Term-mode proof.
563 ext i
564 unfold projectState embedState
565 simp [coupledCoreEquivFin]
566
567/-- Zero-padding is injective. -/