Finger
plain-language theorem explainer
Finger enumerates the ten fingers via five left-hand and five right-hand positions. Cross-domain researchers cite this inductive type when certifying that multiple RS domains realize the 2 times 5 factorization. The definition is a direct inductive construction that derives DecidableEq, Repr, BEq, and Fintype automatically.
Claim. Let $F$ be the inductive type whose elements are the ten fingers: left and right versions of thumb, index, middle, ring, and pinky.
background
Module C17 treats ten-fold combinations as instances of the factorization 10 = 2 × 5 = 2D, where the doubling arises from pairing a five-element structure with a binary orientation or polarity. The Finger type supplies the concrete example for the anatomical domain (five fingers per hand times two hands). HasTenFold is the predicate that a type has cardinality ten; it is used to certify each listed domain instance inside the TenFoldCombinationsCert structure.
proof idea
This is a direct inductive definition that introduces ten constructors and derives the four typeclass instances in a single line.
why it matters
The definition supplies one of the four concrete types collected by TenFoldCombinationsCert, which also records the numerical identity 10 = 2 * 5. It thereby contributes to the structural claim that ten-fold enumerations recur across domains as 2 × 5 factorizations, consistent with the Recognition Science ten-fold wave. The parent result is the certification structure that assembles finger_10, digit_10, lumSac_10, and dBlock_10.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.