alkali_low_ionization
plain-language theorem explainer
Alkali metals are defined by having exactly one valence electron beyond the previous noble-gas closure. A researcher deriving metallic bonding or ionization trends from the Recognition Science framework would cite this to fix the valence count for Li, Na, K, Rb, Cs and Fr. The proof reduces the claim to exhaustive checking of the six-element list after unfolding the alkali-metal definition.
Claim. For any natural number $Z$ in the alkali-metal set $A = [3,11,19,37,55,87]$, the valence-electron count $Z - p(Z)$ equals 1, where $p(Z)$ is the atomic number of the preceding noble-gas closure.
background
AlkaliMetalZ is the finite list [3,11,19,37,55,87] of the alkali metals. ValenceElectrons(Z) is defined as Z minus prevClosure(Z), where prevClosure returns the largest noble-gas atomic number strictly below Z (0 for Z≤2, 2 for Z≤10, 10 for Z≤18, etc.). The metallic-bond module states that metals exhibit low ionization energy so that valence electrons delocalize across the lattice to minimize J-cost and participate in an 8-tick collective rhythm.
proof idea
The term proof first applies simp to replace the membership hypothesis with the explicit list definition of alkaliMetalZ. It then invokes fin_cases on that hypothesis and resolves each of the six concrete cases by native_decide.
why it matters
The result supplies the valence count of one that the module documentation uses to characterize the electron sea in metallic bonding. It directly implements the low-ionization prediction for alkali metals and supports the RS claim that delocalized electrons minimize recognition cost. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.