valenceElectrons
plain-language theorem explainer
The definition computes valence electron count for atomic number Z by subtracting the atomic number of the preceding noble gas from Z. Modelers of periodic trends in Recognition Science cite it when deriving shell closures or radii from the eight-tick ledger without per-element parameters. It is realized as a direct subtraction against the piecewise prevClosure function that hard-codes the noble-gas sequence 0, 2, 10, 18, 36, 54.
Claim. For atomic number $Z$, the valence-electron count is $v(Z) = Z - C(Z)$, where $C(Z)$ is the atomic number of the nearest preceding noble gas (with $C(Z)=0$ for $Z≤2$).
background
The Periodic Table module implements an octave-to-eight-tick mapping for chemistry via φ-tier rails and a fixed set of block offsets. Noble-gas closures are defined as the points where cumulative valence cost meets 8-window neutrality, exactly the chemical image of the fundamental RS scheduler. prevClosure supplies the preceding closure: it returns 0 for Z≤2, 2 for Z≤10, 10 for Z≤18, 18 for Z≤36, 36 for Z≤54, and 54 thereafter.
proof idea
One-line definition that subtracts the value of prevClosure Z from Z. The upstream prevClosure is itself a simple nested conditional that encodes the fixed noble-gas sequence.
why it matters
This definition supplies the valence proxy required by the Noble Gas Closure Theorem (P0-A0) stated in the module doc-comment. It is invoked directly by downstream results such as helium_full_shell, argon_full_shell, krypton_full_shell and the valence-one statements for Cs and Fr. The construction realizes the eight-tick octave (T7) inside the chemical domain and supplies the deterministic input to the alpha-band and mass-ladder predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.