ElectronBlock
plain-language theorem explainer
The inductive definition introduces the five canonical electron blocks of the periodic table. Chemists formalizing periodicity from Recognition Science cite it to fix the block count at five. The construction is direct, with automatic derivation of decidable equality, representation, boolean equality, and finiteness.
Claim. The set of electron blocks consists of five elements: $s$, $p$, $d$, $f$, and $g$ (predicted), equipped with decidable equality and finite cardinality.
background
The module states that electron shell capacities follow the standard formula $2n^2$ for principal quantum number $n$, producing period lengths 2, 8, 8, 18, 18, 32, 32. The number of distinct block types is fixed at five: s, p, d, f, and a predicted g block. This count equals configDim $D=5$, kept separate from the spatial dimension $D=3$ fixed by T8 in the unified forcing chain. The module notes that while capacities are not phi-ladder derived, the block enumeration supports the total of 32 elements in later periods.
proof idea
The declaration is an inductive definition with five constructors. Deriving clauses automatically equip the type with decidable equality, representation, boolean equality, and finiteness instances. No lemmas or tactics are invoked.
why it matters
This supplies the type for the theorem proving cardinality five and for the structure certifying the five blocks together with shell capacities. It fills the chemistry tier by separating block count (5) from capacity formulas ($2n^2$). In the Recognition framework it instantiates configDim $D=5$ for the periodic table, consistent with the eight-tick octave and phi-ladder periods. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.