projectState
projectState defines the linear projection that restricts a state in the N-ququart coupled-core space to its first d coordinates via the canonical finite enumeration. Researchers modeling finite-dimensional approximations or operator lifts in recognition cores cite this when composing embeddings with projections. The definition supplies the pointwise action directly from the basis equivalence, with linearity holding by reflexivity on the function-space operations.
claimLet $d,N$ be natural numbers with $d$ at most the cardinality of the index set of $N$ coupled ququarts. The linear map from the space of functions on configurations (Fin $N$ to Fin 4) to complex $d$-tuples sends a state vector $ψ$ to the vector whose $i$-th entry is $ψ$ evaluated at the preimage under the enumeration bijection of the cast of $i$ into the full index set.
background
CoupledCoreIndex N is the set of all assignments of one of four levels to each of N sites, written Fin N → Fin 4. CoupledCoreSpace N is the complex vector space of all functions from this index set to ℂ, hence a Hilbert space of dimension exactly 4^N. The upstream enumeration coupledCoreEquivFin supplies the explicit bijection from this index set onto Fin (4^N), allowing any finite-dimensional subspace to be identified with the initial segment of the standard basis.
proof idea
The definition installs the toFun clause that composes the input function with the inverse of the enumeration and the castLE truncation. The two linearity axioms are discharged by reflexivity because addition and scalar multiplication act pointwise on the function space.
why it matters in Recognition Science
The definition supplies the left inverse needed for the round-trip identity projectState_embedState and for the injectivity argument in embedState_injective. It is the projection half of the operator-lifting construction liftOperator, which embeds finite-dimensional linear maps into the full coupled-core carrier. Within the Recognition framework this supplies the concrete mechanism for dimensional reduction on ququart chains, consistent with the eight-tick octave and the phi-ladder truncation steps.
scope and limits
- Does not extend the projection to infinite N or non-discrete indices.
- Does not incorporate the J-cost functional or the Recognition Composition Law.
- Does not define the complementary embedding map.
- Does not preserve inner products or other Hilbert-space structure beyond linearity.
formal statement (Lean)
547def projectState {d N : ℕ} (h : d ≤ Fintype.card (CoupledCoreIndex N)) :
548 CoupledCoreSpace N →ₗ[ℂ] (Fin d → ℂ) where
549 toFun := fun ψ i => ψ ((coupledCoreEquivFin N).symm (Fin.castLE h i))
proof body
Definition body.
550 map_add' := by
551 intro ψ χ
552 ext i
553 rfl
554 map_smul' := by
555 intro z ψ
556 ext i
557 rfl
558
559/-- Projection recovers the original state after zero-padding. -/