DBlockElement
plain-language theorem explainer
The inductive type enumerates the ten elements of the first d-block period as an instance of the 2·5 factorization. Cross-domain researchers cite it when certifying that multiple RS structures share cardinality 10. The definition is a direct enumeration of ten constructors together with automatic derivation of decidable equality and finite type.
Claim. Let $DBlockElement$ be the set whose elements are the ten chemical species scandium through zinc that occupy the first d-block row of the periodic table.
background
The module establishes that many Recognition Science domains satisfy a universal ten-fold enumeration 10 = 2·5. One listed instance is the periodic table, where each d-block period contributes exactly ten elements. The sibling predicate HasTenFold is the interface that records this cardinality for any such domain. The upstream period definition supplies the exponential scaling used elsewhere in the astrophysics layer but is not invoked by this enumeration.
proof idea
Direct inductive definition that introduces ten named constructors and derives DecidableEq, Repr, BEq and Fintype in a single line.
why it matters
Supplies the dBlock_10 field required by the TenFoldCombinationsCert structure that collects all ten-fold examples and records the explicit factorization 10 = 2·5. It thereby completes the periodic-table entry in the module's list of cross-domain instances of the 2D pattern. No open scaffolding remains for this particular case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.