tenfold_squared
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not establish that all 10-fold structures are isomorphic beyond cardinality.
- Does not extend to infinite sets or non-finite types.
- Does not compute explicit bijections between different 10-fold instances.
- Does not address higher-order products or powers of such sets.
formal statement (Lean)
68theorem tenfold_squared
69 {A B : Type} [Fintype A] [Fintype B]
70 (hA : HasTenFold A) (hB : HasTenFold B) :
71 Fintype.card (A × B) = 100 := by
proof body
Term-mode proof.
72 unfold HasTenFold at hA hB
73 simp [Fintype.card_prod, hA, hB]
74
75/-- 10 × D = 50. 50 is still below gap45+5. -/