alkali_min_valence
plain-language theorem explainer
Alkali metals lithium (Z=3), sodium (Z=11), and potassium (Z=19) each possess exactly one valence electron, computed as the difference from the preceding noble-gas closure. Recognition Science chemists cite this to ground the prediction that these elements show the lowest electronegativity within their periods under φ-ladder scaling of shell distance. The proof is a direct native_decide evaluation of the valenceElectrons definition at these three atomic numbers.
Claim. The valence electron counts satisfy $v(3)=1$, $v(11)=1$, and $v(19)=1$, where $v(Z)$ denotes the number of electrons beyond the previous noble-gas core, $v(Z) := Z - $ prevClosure$(Z)$.
background
In the Recognition Science module on electronegativity from φ-ladder scaling, electronegativity is modeled as EN ~ distToNextClosure^{-1} modulated by shell number, with classical Mulliken form EN ~ √(IE × EA) recovered as a limit. The valence electron count for atomic number Z is defined as the electrons beyond the prior noble-gas closure, so that noble gases occur precisely where this count equals the period length. Alkali metals sit immediately after noble gases and therefore carry valence count 1, placing them farthest from the next shell closure within each period.
proof idea
The proof is a one-line term that applies native_decide to evaluate the conjunction of valenceElectrons 3, valenceElectrons 11, and valenceElectrons 19 directly from the upstream definition valenceElectrons Z = Z - prevClosure Z.
why it matters
This theorem supplies the concrete anchor for the CH-008 prediction that alkali metals exhibit the lowest electronegativity in their periods and that EN decreases down a group. It feeds the sibling ranking theorems (enRanking, en_increases_across_period) and the general pattern that EN increases toward shell closure. The result is consistent with the φ-ladder and eight-tick octave structure of shell filling but does not itself derive the scaling law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.