blockElectronCount
Block electron counts are assigned by direct pattern match on the four block types: two electrons for s, six for p, ten for d, and fourteen for f. Chemists building fit-free periodic-table predictions inside Recognition Science cite this assignment when constructing the valence ledger. The definition is realized as exhaustive case analysis on the Block inductive type.
claimLet $b$ range over the blocks $s,p,d,f$. The electron count function is defined by $n(s)=2$, $n(p)=6$, $n(d)=10$, $n(f)=14$.
background
The Block inductive type consists of four constructors s, p, d, f that label the angular-momentum blocks with fixed φ-packing offsets. The Periodic Table module supplies a zero-parameter engine that maps the eight-tick octave of Recognition Science onto chemical shell closures via an eight-window neutrality predicate. Upstream, the Block definition itself records the structural offsets required by the forcing chain.
proof idea
The definition is realized by exhaustive pattern matching on the four constructors of the Block inductive type, returning the corresponding natural number in each branch.
why it matters in Recognition Science
This definition supplies the concrete counts consumed by the block_count_formula theorem, which recovers the standard 2(2l+1) expression. It thereby supports the Noble Gas Closure Theorem (P0-A0) stated in the module, furnishing the deterministic valence proxy that forces the observed noble-gas sequence {2,10,18,36,54,86} from eight-tick ledger balance.
scope and limits
- Does not assign specific atomic numbers to blocks.
- Does not compute energies, offsets, or ionization potentials.
- Does not encode exceptions to Aufbau order.
- Does not reference measured data or empirical fitting.
formal statement (Lean)
229def blockElectronCount : Block → ℕ
230 | Block.s => 2
231 | Block.p => 6
232 | Block.d => 10
233 | Block.f => 14
234
235/-- Block counts follow 2(2l+1) for angular momentum quantum number l. -/