DecimalDigit
plain-language theorem explainer
DecimalDigit defines an inductive type with exactly ten constructors d0 through d9. Researchers working on cross-domain enumerations in Recognition Science cite it when certifying that multiple structures (digits, fingers, spinal levels, d-block elements) share cardinality 10 = 2·5. The declaration is a plain inductive definition that automatically derives DecidableEq, Repr, BEq and Fintype.
Claim. Let $D$ be the inductive type whose elements are the ten decimal digits, generated by the constructors $d_0, d_1, d_2, d_3, d_4, d_5, d_6, d_7, d_8, d_9$.
background
The module C17 establishes that several Recognition Science domains enumerate to cardinality 10, factorised universally as 10 = 2·5. One listed instance is the ten decimal digits. HasTenFold is the predicate (defined in the same module) asserting that a type satisfies this ten-fold property. The module imports only Mathlib and contains no upstream theorems; the local setting is the structural claim that 10 arises repeatedly as the product of a five-element structure with an orientation or alternation.
proof idea
Inductive definition that enumerates the ten cases d0 to d9 and derives the required type-class instances via the deriving clause.
why it matters
Supplies the concrete type used by digit_is_10 to witness HasTenFold DecimalDigit and by TenFoldCombinationsCert to collect four independent ten-fold instances together with the factorisation (10 : ℕ) = 2 * 5. It therefore contributes one concrete datum to the C17 cross-domain claim that 10 = 2D appears in cancer hallmarks, sense types, fingers, commandments, spinal levels and periodic-table blocks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.