alkaliMetalZ
plain-language theorem explainer
The definition enumerates the atomic numbers of the alkali metals as the list [3, 11, 19, 37, 55, 87]. Chemists modeling metallic bonding or ionic compounds within Recognition Science cite this list to select species with minimal ionization energy and single valence electrons. It is supplied as a direct constant list with no computation or reduction steps.
Claim. The alkali metals are the elements whose atomic numbers belong to the finite set $S = [3, 11, 19, 37, 55, 87]$.
background
In the Recognition Science treatment of metallic bonding, valence electrons delocalize across a lattice of cations to minimize J-cost rather than localize on individual atoms. The module links this delocalization to the eight-tick coherence of the electron sea and to phi-related scaling of conductivity. The same list appears upstream in IonicBond and IonizationEnergy, where the doc-comment states that alkali metals (Li, Na, K, Rb, Cs, Fr) have low ionization energy.
proof idea
The declaration is a direct definition that enumerates the six atomic numbers with no lemmas, tactics, or reductions applied.
why it matters
The list supplies the input set for predicates such as isAlkaliMetal and for theorems such as alkali_halogen_ionic that establish ionic bonding via electronegativity differences. It anchors the metallic-bonding derivation to the eight-tick octave and to the low-ionization-energy regime required for electron delocalization. The definition closes the interface between periodic-table data and Recognition Science predictions for conductivity proxies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.