tenfold_equicardinal
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not establish that any concrete domain satisfies HasTenFold.
- Does not extend beyond finite types.
- Does not produce explicit bijections between the sets.
- Does not address non-finite or infinite cases.
formal statement (Lean)
61theorem tenfold_equicardinal
62 {A B : Type} [Fintype A] [Fintype B]
63 (hA : HasTenFold A) (hB : HasTenFold B) :
64 Fintype.card A = Fintype.card B := by
proof body
Term-mode proof.
65 rw [hA, hB]
66
67/-- 10 × 10 = 100. -/