coupledCoreIndex_card
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.