coupledCoreIndex_card
The cardinality of the coupled-core index space for any natural number N is exactly 4 to the power N. Researchers constructing exact embeddings of finite-dimensional linear operators into ququart tensor carriers cite this count to select the minimal number of cores. The proof is a direct simplification that unfolds the index type definition.
claimFor every natural number $N$, the finite cardinality of the coupled-core index space satisfies $|CoupledCoreIndex(N)| = 4^N$.
background
CoupledCoreIndex N labels the standard basis of the tensor product of N ququarts, each a four-level system whose states are indexed by elements of Fin 4. The type is constructed inductively so that its Fintype.card equals 4^N by definition. This cardinality statement lives in the CoupledRecognitionCores module and is re-exported into the OperatorCore layer to support linear-algebraic constructions.
proof idea
The declaration is an abbreviation that re-exports the theorem from CoupledRecognitionCores. The underlying proof applies the simp tactic to the definition of CoupledCoreIndex, which immediately yields the power-of-four cardinality.
why it matters in Recognition Science
This cardinality supplies the dimension bound used by the finite-dimensional exact embedding theorem, which embeds any linear map on a d-dimensional space into the coupled-core carrier of size 4^d. It anchors the framework's use of ququart tensors as finite carriers for recognition dynamics and closes the counting step required for exact operator embeddings.
scope and limits
- Does not exhibit an explicit basis or phase factors for the index space.
- Does not treat infinite-dimensional or continuous-index extensions.
- Does not construct the embedding map or prove its linearity.
Lean usage
by simpa [coupledCoreIndex_card] using self_le_four_pow_self dformal statement (Lean)
20abbrev coupledCoreIndex_card := IndisputableMonolith.Foundation.CoupledRecognitionCores.coupledCoreIndex_card