cs_valence_one
plain-language theorem explainer
Cesium has exactly one valence electron by the Recognition Science definition subtracting the prior noble gas core from atomic number. Chemists modeling alkali metal radii trends in the phi-ladder framework would cite this to anchor group-one behavior. The verification is a direct native computation of the valenceElectrons function at Z=55.
Claim. Cesium (atomic number 55) has one valence electron beyond the previous noble gas core: valence electrons of cesium equal 1.
background
Recognition Science derives atomic radii from phi-ladder scaling of coherence lengths, with period trends decreasing radii across a row and group trends increasing them down a column via new shells. The valenceElectrons function is defined as Z minus prevClosure Z, counting electrons outside the last closed shell; at noble gases this count equals the period length, matching the RS insight that closed shells occur precisely when valence equals period length. The module sets this within CH-007, where effective radii also decrease with valence electrons due to screening penetration.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic definition of valenceElectrons at 55.
why it matters
This result belongs to the series of alkali-metal valence checks (Li, Na, K, Rb, Cs) that confirm the periodic table structure underlying phi-ladder radius predictions. It supports the module's claim that alkali metals exhibit maximal radii after noble-gas closures because a new shell begins. No downstream theorems are recorded, leaving open whether these facts will be folded into a general radius formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.