localWeylFamily_card
plain-language theorem explainer
The collection of local Weyl family elements, indexed by pairs from two 4-element sets, contains precisely 16 members. Workers on coupled recognition cores cite this when sizing the operator algebra for ququart states. The proof reduces to a direct finite-set cardinality computation.
Claim. The cardinality of the Cartesian product of two 4-element finite sets is 16.
background
The CoupledRecognitionCores module defines structures for ququart states and their basis kets, with the local Weyl family serving as the index set for the associated operator family. This sits within the broader Recognition Science setting where discrete finite structures emerge from the phi-forcing chain and J-cost minimization. Upstream lemmas on spectral emergence confirm the appearance of 24 fermion flavors and related discrete counts that motivate such finite cardinalities.
proof idea
A one-line wrapper applies the decide tactic to evaluate the product cardinality directly from the definitions of Fin 4.
why it matters
This result feeds the alias in the OperatorCore module for use in coupled cores. It instantiates the expected dimension 16 for the local Weyl family, consistent with the eight-tick octave and D=3 spatial dimensions in the forcing chain. It closes a basic counting step without open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.