coupledCoreIndex_card
plain-language theorem explainer
The cardinality of the configuration space of N coupled ququart cores equals exactly 4^N. Researchers embedding finite-dimensional linear dynamics into recognition core carriers cite this bound to guarantee sufficient capacity. The proof is a one-line simplification that unfolds the definition of CoupledCoreIndex as the function type Fin N to Fin 4.
Claim. For every natural number $N$, the cardinality of the set of functions from a set of $N$ elements to a set of four elements is $4^N$.
background
CoupledCoreIndex N is the finite-site configuration space of coupled ququart cores, defined as the function type Fin N → Fin 4. This type serves as the concrete index set for the Hilbert carrier of N coupled recognition cores in the CoupledRecognitionCores module. The surrounding development imports basic Mathlib structures and relies on the phase definitions from EightTick and the RiemannHypothesis.Wedge module to support the broader operator algebra, although those phases are not invoked in the cardinality step itself.
proof idea
The proof is a one-line wrapper that applies simp to the abbreviation CoupledCoreIndex, reducing the claim directly to the standard Fintype.card computation for the finite function space Fin N → Fin 4.
why it matters
This cardinality result is invoked by the finite-dimensional exact embedding theorem, which constructs an exact linear embedding of any d-dimensional dynamics into the coupled-core space of dimension 4^d. It supplies the dimension-counting step required for the foundation of exact embeddings of linear maps into recognition cores and connects to the eight-tick octave structure through the ququart basis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.