na_valence_one
plain-language theorem explainer
Sodium (Z=11) has exactly one valence electron under the definition that subtracts the preceding noble-gas closure from atomic number. Chemists modeling alkali-metal placement in the RS periodic table cite this to confirm group-1 membership for radius-maxima predictions. The proof is a direct native_decide evaluation of the valenceElectrons function.
Claim. The number of valence electrons for the element with atomic number 11 equals 1, where valence electrons are defined as atomic number minus the atomic number of the preceding noble-gas core.
background
The Chemistry.AtomicRadii module derives atomic radii from φ-ladder scaling: base radius grows with shell number while effective radius shrinks with valence electrons via screening. The upstream valenceElectrons definition computes Z minus prevClosure Z, counting electrons outside the last closed shell. Its doc-comment states that noble gases occur exactly when this count equals the period length, supplying the RS insight that alkali metals begin each new shell with one valence electron.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the valenceElectrons definition at Z=11 and confirm the result is 1.
why it matters
This theorem belongs to the alkali-metal verification chain (li_valence_one through cs_valence_one) inside the atomic-radii module. It supplies the concrete instance of the CH-007 claim that new shells produce radius maxima down a group, consistent with the φ-ladder and coherence-length scaling. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.