HasTenFold
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert that any concrete type satisfies the predicate.
- Does not derive the factorization 10 = 2 · 5 from the J-function or forcing chain.
- Does not apply to infinite types or non-finite structures.
- Does not connect cardinality to mass formulas or Berry creation thresholds.
Lean usage
theorem finger_is_10 : HasTenFold Finger := by unfold HasTenFold; decideformal statement (Lean)
29def HasTenFold (T : Type) [Fintype T] : Prop := Fintype.card T = 10
proof body
Definition body.
30