tenfold_equicardinal
plain-language theorem explainer
Any two finite types each carrying 10-fold structure share identical cardinality. Cross-domain researchers cite the result when equating enumerations such as fingers with decimal digits or sense types with spinal levels. The proof is a one-line rewrite that substitutes the defining cardinality equalities from the two HasTenFold hypotheses.
Claim. If $A$ and $B$ are finite types each satisfying the 10-fold condition, then the cardinality of $A$ equals the cardinality of $B$.
background
The module records that multiple Recognition Science domains enumerate to exactly 10 elements under the factorization 10 = 2 · 5 = 2D. HasTenFold is the predicate on a finite type T asserting that its cardinality equals 10. This supplies the only hypotheses needed for the present theorem.
proof idea
The proof is a one-line rewrite that substitutes the two HasTenFold hypotheses into the goal, replacing both cardinalities by 10.
why it matters
The lemma anchors the ten-fold combinations module by confirming that all listed 10-element structures are interchangeable in size. It fills the structural claim 10 = 2 · 5 = 2D, where the doubling pairs a 5-element structure with an orientation or alternation. No downstream uses appear yet, but the result supports equating instances such as the 10 Hallmarks of Cancer with the 10 sense types.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.