tenfold_squared
plain-language theorem explainer
The theorem establishes that the Cartesian product of any two finite sets each of cardinality 10 has cardinality 100. Researchers working on cross-domain enumerations in Recognition Science cite it when combining 10-fold structures such as decimal digits with fingers or d-block elements. The proof is a direct term-mode simplification that unfolds the cardinality hypotheses and applies the product rule for finite types.
Claim. If $A$ and $B$ are finite sets with $|A|=10$ and $|B|=10$, then $|A×B|=100$.
background
The Ten-Fold Combinations module collects instances across domains that each enumerate to cardinality 10, factorable as 2·5. The predicate HasTenFold on a finite type T asserts that its cardinality equals 10, supplying the hypothesis for both factors in the product. This lemma sits inside the structural claim that 10 equals 2 times D, appearing in examples such as 10 fingers, 10 decimal digits, 10 lumbar-sacral levels, and 10 d-block elements per period.
proof idea
The proof unfolds the HasTenFold hypotheses for A and B to expose the two cardinality equalities, then applies the standard simplification rule for the cardinality of a Cartesian product together with those equalities.
why it matters
This result is used by the tenFoldCombinationsCert definition that aggregates the 10-fold properties. It fills the C17 claim that many RS domains enumerate to 10 = 2·5. Within the Recognition framework it reinforces the universal factorisation used in cross-domain arguments, consistent with the eight-tick octave and the D = 3 spatial dimensions derived elsewhere in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.