dBlock_is_10
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the 10-fold property from the J-cost or Recognition Composition Law.
- Does not extend the count to higher periods or other blocks.
- Does not address whether the 2·5 factorisation is forced by the T0–T8 chain.
- Does not prove uniqueness of the d-block enumeration among chemical sets.
Lean usage
dBlock_10 := dBlock_is_10formal statement (Lean)
54theorem dBlock_is_10 : HasTenFold DBlockElement := by
proof body
Term-mode proof.
55 unfold HasTenFold; decide
56
57/-- 10 = 2 · 5 factorisation. -/