localWeylFamily_card
plain-language theorem explainer
The local Weyl family on pairs of 4-element index sets has cardinality 16. Researchers constructing coupled recognition cores cite this to fix the dimension of the local operator basis before building tensor products and relations. The result follows from a direct finite-set enumeration.
Claim. The cardinality of the finite type $Fin 4 × Fin 4$ equals 16.
background
This abbrev sits in the OperatorCore module for coupled recognition cores and imports the core definitions from CoupledRecognitionCores. Sibling declarations include ququartWeyl_relation, localWeylMonomial, and tensorWeylMonomial, which index operators on ququart states (4-level systems). The upstream theorem states that the local Weyl family has the expected cardinality 16.
proof idea
This is a one-line abbreviation that re-exports the cardinality theorem from the CoupledRecognitionCores module. The underlying proof applies the decide tactic to verify Fintype.card (Fin 4 × Fin 4) = 16.
why it matters
The cardinality anchors the size of the local Weyl family used in coupled-core operator constructions. It supports the same-named result and downstream relations such as ququartWeyl_relation. The fact contributes to the finite-dimensional foundation before any scaling by the phi-ladder or eight-tick octave appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.