blockElectronCount
plain-language theorem explainer
blockElectronCount supplies the electron capacities for the four orbital blocks in the Recognition Science periodic table model; derivations of shell closures and valence ledgers cite this mapping to enforce eight-window neutrality; the definition is a direct exhaustive case split on the four constructors of the Block inductive type.
Claim. The function assigning electron counts to blocks is defined by $blockElectronCount(s)=2$, $blockElectronCount(p)=6$, $blockElectronCount(d)=10$, $blockElectronCount(f)=14$.
background
The PeriodicTable module supplies a zero-parameter scaffold that maps the eight-tick octave of Recognition Science onto chemical shell structure via φ-tier rails and an eight-window neutrality predicate. Noble gases are defined exactly as the points where cumulative valence cost returns to zero modulo 8. The Block inductive type enumerates the four orbital blocks s, p, d, f with fixed φ-packing offsets and no per-element tuning permitted.
proof idea
The definition is realized by direct pattern matching on the four constructors of the Block inductive type, returning the respective natural numbers.
why it matters
blockElectronCount is invoked by the downstream theorem block_count_formula that equates the counts to the standard 2(2l+1) expression. It supplies the deterministic valence proxy required by the Noble Gas Closure Theorem (P0-A0) stated in the module documentation. The construction thereby embeds the T7 eight-tick octave into the chemical ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.