CoupledCoreIndex
plain-language theorem explainer
CoupledCoreIndex supplies the configuration space for N coupled ququart cores as maps from site indices to four local states. Researchers modeling finite-dimensional coupled systems in Recognition Science cite it to index basis vectors and displacements. The declaration is a one-line alias to the upstream definition Fin N → Fin 4.
Claim. For a natural number $N$, the coupled-core index is the set of all functions from the finite set of $N$ sites to the four-element set of local states: $CoupledCoreIndex(N) := (Fin N) → (Fin 4)$.
background
The CoupledRecognitionCores module introduces the finite-site configuration space of coupled ququart cores. Each core occupies one of four states, so a global configuration for N cores is a function assigning a state in Fin 4 to each site in Fin N. The upstream doc-comment states: 'The finite-site configuration space of coupled ququart cores.'
proof idea
This is a one-line alias that re-exports the definition CoupledCoreIndex (N : ℕ) := Fin N → Fin 4 from the imported CoupledRecognitionCores module.
why it matters
The type appears in 29 downstream declarations, including addedConfig for displacements, coupledBasisKet for standard basis vectors, and coupledCoreEquivFin for enumeration by Fin. It supplies the index set required for the Hilbert carrier CoupledCoreSpace N and for shift and orthonormality results that support the finite-dimensional models in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.