digit_is_10
plain-language theorem explainer
The declaration shows that the decimal digits type has exactly ten elements, satisfying the ten-fold structure predicate. Cross-domain researchers in Recognition Science cite it to group decimal digits with fingers, spinal levels, and d-block elements under the common factorization 10 = 2 × 5. The proof proceeds by unfolding the cardinality definition and deciding the resulting equality.
Claim. Let DecimalDigit be the inductive type with ten constructors d0 through d9. Then Fintype.card(DecimalDigit) = 10.
background
HasTenFold T is the proposition that a finite type T has cardinality exactly 10, equivalently 2 times 5. DecimalDigit is the inductive type with ten constructors d0 to d9 that derives a Fintype instance, so its cardinality is immediately decidable. Module C17 collects instances of this ten-fold enumeration across domains, including sense types, fingers, lumbar-sacral levels, and d-block elements, all sharing the factorization 10 = 2 · 5.
proof idea
The proof is a one-line wrapper that unfolds HasTenFold to the equation Fintype.card DecimalDigit = 10 and then applies decide to verify the equality on the ten-element inductive type.
why it matters
This theorem supplies one field in the tenFoldCombinationsCert bundle that aggregates four concrete ten-fold instances plus the factoring lemma ten_eq_two_D. It directly supports the C17 structural claim that 10 = 2 · 5 appears uniformly across RS domains. The result sits alongside the eight-tick octave and D = 3 landmarks but leaves open the dynamical origin of the doubling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.