dBlock_is_10
plain-language theorem explainer
The theorem shows that the inductive type of first-period d-block elements has cardinality exactly 10, satisfying the 10-fold predicate. Cross-domain cataloguers in Recognition Science cite it when listing instances of the universal 2·5 factorisation across chemistry, biology, and axial structures. The proof is a one-line wrapper that unfolds the cardinality predicate and invokes decidability to confirm the count.
Claim. Let $D$ be the finite set of first-period d-block elements. Then $|D| = 10 = 2·5$.
background
HasTenFold is the predicate on a finite type T asserting that its cardinality equals 10, equivalently 2·5. DBlockElement is the inductive type whose ten constructors are the first-period d-block elements scandium through zinc. The module C17 frames these as one of several cross-domain enumerations that all realise the same 10 = 2·5 factorisation, with the doubling arising from pairing a 5-element structure with an orientation or alternation.
proof idea
One-line wrapper that unfolds HasTenFold and applies decide to the decidable equality on the Fintype instance of DBlockElement.
why it matters
The result populates the tenFoldCombinationsCert record, which aggregates all 10-fold instances and records the common 2·5 factorisation. It supplies concrete chemical support for the structural claim in C17 that many RS domains enumerate to 10 = 2·D, consistent with the eight-tick octave and the emergence of D = 3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.