digit_is_10
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not derive the number 10 from the J-uniqueness or phi fixed-point equation.
- Does not supply a mechanism that generates ten-fold structures from lower-level forcing steps.
- Does not extend the claim to infinite or continuous settings.
- Does not link the cardinality directly to the mass ladder or alpha band.
Lean usage
digit_10 := digit_is_10formal statement (Lean)
50theorem digit_is_10 : HasTenFold DecimalDigit := by
proof body
One-line wrapper that applies unfold.
51 unfold HasTenFold; decide