block_count_formula
plain-language theorem explainer
The theorem equates the electron counts assigned to s, p, d, f blocks with the standard spectroscopic formula 2(2l+1) for l=0,1,2,3. Periodic-table modelers working in Recognition Science would cite it to confirm that the fixed block definitions reproduce textbook orbital capacities. The proof is a one-line term proof that performs exhaustive case analysis on the Block inductive type and closes by reflexivity.
Claim. For each block type $b$, the electron count $n(b)$ satisfies $n(s)=2$, $n(p)=6$, $n(d)=10$, $n(f)=14$, which is identical to the formula $2(2l+1)$ with orbital angular momentum quantum number $l=0,1,2,3$ respectively.
background
The module implements a fit-free periodic-table engine that maps the Recognition Science eight-tick octave onto chemical blocks. Block is the inductive type with four constructors s, p, d, f that carry fixed phi-packing offsets. The sibling definition blockElectronCount directly returns the integers 2, 6, 10, 14 for these constructors. The surrounding module doc states that noble-gas closures occur exactly where cumulative valence cost meets 8-window neutrality, the chemical counterpart of the RS 8-tick ledger balance.
proof idea
The term proof performs case analysis on the input block b, dispatching to each of the four constructors, then applies reflexivity to match the right-hand side of the definition of blockElectronCount.
why it matters
The result anchors the chemistry scaffold to standard angular-momentum counting, thereby supporting the Noble Gas Closure Theorem (P0-A0) that forces the set {2,10,18,36,54,86} from 8-window neutrality alone. It supplies the concrete block capacities required by the eight-tick octave (T7) and the D=3 spatial structure of the Recognition framework without introducing free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.