li_valence_one
plain-language theorem explainer
Lithium (atomic number 3) has exactly one valence electron under the Recognition Science definition that subtracts the prior noble-gas closure from Z. This supplies the base case confirming alkali metals open each new shell with valence one. The verification is a direct computational check via native_decide on the difference Z minus prevClosure Z.
Claim. The valence-electron count for the element with atomic number 3 satisfies $valenceElectrons(3)=1$, where $valenceElectrons(Z)$ is defined as the number of electrons beyond the preceding noble-gas core closure.
background
Valence electrons for atomic number Z are given by the difference Z minus the atomic number of the preceding noble-gas closure. This definition encodes the Recognition Science view that noble gases mark complete shells and that alkali metals therefore begin each new shell with valence one. The module develops atomic radii from φ-ladder scaling, with radii increasing down groups as new shells open farther from the nucleus and decreasing across periods as nuclear charge rises.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the concrete integer value of valenceElectrons 3 and confirm equality to 1.
why it matters
This supplies the base case for the alkali-metal valence pattern that drives the group trend of increasing atomic radii in the φ-ladder model. It directly supports the module statement that alkali metals exhibit local maxima after noble gases because new shells start. No downstream theorems yet reference the result, leaving open the generalization to heavier alkalis and the explicit radius formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.