finger_is_10
Finger enumeration satisfies the ten-fold cardinality condition in the cross-domain module. Researchers cataloging 2·5 factorizations across biology and structure would cite this result. The proof reduces the claim to a decidable equality on the finite type by unfolding the predicate.
claimLet $F$ be the type consisting of ten fingers (five left-hand and five right-hand variants). Then the cardinality of $F$ equals 10.
background
The TenFoldCombinations module documents structural instances where domains enumerate to 10 = 2·5, including fingers, digits, and d-block elements. HasTenFold is the predicate asserting that a finite type has cardinality exactly 10. Finger is the inductive type with ten constructors for the paired fingers. This setting supports the claim that the doubling arises from pairing a 5-element structure with an orientation or polarity, as stated in the module documentation.
proof idea
The proof is a one-line wrapper. It unfolds HasTenFold to the equality Fintype.card Finger = 10 and invokes the decide tactic, which succeeds on the explicitly finite inductive type.
why it matters in Recognition Science
The result supplies the finger instance to the tenFoldCombinationsCert certificate that aggregates multiple ten-fold verifications. It realizes the C17 claim of ten-fold combinations in the module, linking to the universal factorization 10 = 2·D. Within Recognition Science this instance illustrates the cross-domain reach of the 2·5 pattern without invoking the phi-ladder or forcing chain directly.
scope and limits
- Does not prove ten-fold structure for the other domains in the module such as decimal digits.
- Does not connect the finger count to the J-uniqueness or Recognition Composition Law.
- Does not address potential links to the eight-tick octave or spatial dimensions.
- Does not provide a general mechanism for generating all 2·5 enumerations.
Lean usage
example : HasTenFold Finger := finger_is_10formal statement (Lean)
48theorem finger_is_10 : HasTenFold Finger := by
proof body
One-line wrapper that applies unfold.
49 unfold HasTenFold; decide