DBlockElement
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not claim that every period of the periodic table contains exactly these ten d-block elements.
- Does not derive the ten-fold cardinality from the Recognition Composition Law or from J-cost.
- Does not connect the enumeration to the phi-ladder mass formula or to defect distance.
- Does not address higher-period d-block or f-block elements.
formal statement (Lean)
44inductive DBlockElement where
45 | sc | ti | v | cr | mn | fe | co | ni | cu | zn -- first d-block period
46 deriving DecidableEq, Repr, BEq, Fintype
47