CoupledCoreSpace
plain-language theorem explainer
The declaration defines the Hilbert space for N coupled ququart cores as the set of all functions from their finite configuration index to the complex numbers. Researchers embedding linear dynamics or lifting operators in the Recognition framework cite this carrier when constructing finite-dimensional representations. The definition is a direct abbreviation that composes the index set with codomain ℂ.
Claim. Let $I_N := (Fin N) → (Fin 4)$ denote the configuration space of $N$ ququarts. The coupled-core Hilbert space is the vector space of all functions $I_N → ℂ$.
background
In the CoupledRecognitionCores module the index space is defined as CoupledCoreIndex N := Fin N → Fin 4, the set of all assignments of one of four discrete states to each of N sites. This models the finite configuration space of coupled recognition cores, each treated as a ququart. The module sits in the foundation layer and imports Mathlib together with upstream structures from NucleosynthesisTiers and LedgerFactorization that calibrate physical quantities to φ-tiers.
proof idea
This is a one-line abbreviation that substitutes the definition of CoupledCoreIndex N into the function type with codomain ℂ. No lemmas or tactics are invoked.
why it matters
The definition supplies the concrete state space on which all coupled-core operators act and feeds directly into coupledBasisKet, embedState, liftOperator, and finite_dimensional_exact_embedding. It realizes the exact embedding of any d-dimensional linear map by taking N = d, since d ≤ 4^d. Within the Recognition framework it provides the Hilbert carrier for ququart-based representations consistent with the discrete φ-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.