DBlockElement
plain-language theorem explainer
The inductive type enumerates the ten first-series d-block elements. It is cited by the HasTenFold theorem for this type and by the TenFoldCombinationsCert structure that assembles all cardinality-10 instances. The definition is a direct enumeration of ten constructors together with derived decidability and finiteness instances.
Claim. Let $D$ be the inductive type whose ten constructors are scandium, titanium, vanadium, chromium, manganese, iron, cobalt, nickel, copper and zinc, representing the d-block elements of the first transition period.
background
The module establishes that multiple structures in distinct domains each have cardinality 10, universally factorized as $10=2·5$. The listed instances include fingers, decimal digits, lumbar-sacral vertebrae and the d-block elements of the periodic table. The single upstream dependency supplies the phi-power period function used in related astrophysical scaling, though it is not invoked inside this declaration.
proof idea
The declaration is a direct inductive definition that lists the ten constructors explicitly. The four deriving clauses for DecidableEq, Repr, BEq and Fintype are attached automatically; no lemmas or tactics are applied.
why it matters
This definition supplies the d-block case required by dBlock_is_10 and by the TenFoldCombinationsCert structure that certifies the 2·5 factorization across domains. It realizes one concrete instance of the module's structural claim that 10 arises repeatedly as 2 times 5, consistent with the Recognition Science counting that follows from the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.