DecimalDigit
DecimalDigit defines the inductive type with ten constructors d0 through d9. Researchers establishing cross-domain cardinality claims in Recognition Science cite it to instantiate the 10 = 2 × 5 factorization for the decimal digits. The definition proceeds by direct enumeration of constructors with automatic derivation of decidable equality and finite-type instances.
claimLet $D$ be the inductive type whose constructors are the ten elements $d_0, d_1, d_2, d_3, d_4, d_5, d_6, d_7, d_8, d_9$, equipped with decidable equality, representation, boolean equality, and finite-type structure.
background
The module states the structural claim C17 that many Recognition Science domains enumerate to cardinality 10, universally factorized as 10 = 2 × 5. The doubling arises from pairing a five-element structure with an orientation, polarity, or alternation. Concrete instances listed include the ten decimal digits (0-9), ten fingers, ten lower spinal levels, and ten d-block elements per period. HasTenFold is the predicate, used downstream, that asserts a type has exactly ten elements.
proof idea
The declaration is a direct inductive definition that enumerates the ten constructors d0 to d9 and derives the required instances via the deriving clause.
why it matters in Recognition Science
This supplies one of the four instances collected inside the TenFoldCombinationsCert structure, which certifies the factorization 10 = 2 * 5 across domains. It supports the broader claim that 10 arises as 2D in the framework, consistent with the eight-tick octave and dimensional doubling. The immediate parent is the digit_is_10 theorem that establishes HasTenFold for this type.
scope and limits
- Does not assert any physical interpretation of the digits beyond enumeration.
- Does not prove cardinality; that is supplied by the downstream digit_is_10 theorem.
- Does not define arithmetic operations or relations on the digits.
- Does not address other bases or non-decimal enumerations.
formal statement (Lean)
36inductive DecimalDigit where
37 | d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9
38 deriving DecidableEq, Repr, BEq, Fintype
39