HasTenFold
plain-language theorem explainer
HasTenFold is the predicate on finite types that holds precisely when cardinality equals 10. Cross-domain enumerations in Recognition Science cite it to certify recurring 2·5 patterns such as fingers, decimal digits, and d-block elements. The definition is a direct abbreviation to the Fintype.card equality with no additional lemmas required.
Claim. A finite type $T$ has ten-fold structure when its cardinality satisfies $|T| = 10$.
background
The CrossDomain.TenFoldCombinations module establishes that multiple Recognition Science domains enumerate to 10 = 2 · 5. Concrete instances listed include five fingers per hand paired across two hands, five lumbar plus five sacral vertebrae, five external plus five internal sense types, and ten d-block elements per period. The universal factorization is presented as 10 = 2 × D with D = 5 supplying the structural doubling via orientation or alternation.
proof idea
The definition is a direct abbreviation that sets HasTenFold T to the proposition Fintype.card T = 10. No lemmas are invoked and no tactics are executed; the body is a single equality that downstream theorems unfold and discharge by decision procedures.
why it matters
This definition supplies the reusable predicate for the C17 ten-fold claim and is invoked by the certification structure TenFoldCombinationsCert together with equicardinality results such as tenfold_equicardinal. It anchors the cross-domain unification under the eight-tick octave by exhibiting the invariant 10 = 2 · 5 across independent enumerations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.