isAlkaliMetal
plain-language theorem explainer
The predicate identifies natural numbers Z belonging to the alkali metal group via membership in the fixed list of atomic numbers for Li, Na, K, Rb, Cs and Fr. Chemists deriving ionic bond formation within Recognition Science cite it to mark the low-ionization-energy donor in electron-transfer pairs. The definition is realized as a direct membership test against the precomputed alkaliMetalZ list.
Claim. For a natural number $Z$, the predicate holds if and only if $Z$ equals one of 3, 11, 19, 37, 55 or 87.
background
The module derives ionic bond formation from the Recognition Science 8-tick shell-closure mechanism. Alkali metals donate one valence electron to reach noble-gas configuration while halogens accept one to complete their shell; the net energy balance is ionization cost minus electron affinity, stabilized by Madelung lattice energy. The predicate marks the alkali-metal side of this transfer by testing membership in the list [3, 11, 19, 37, 55, 87].
proof idea
One-line definition that applies set membership to the alkali-metal atomic-number list defined in the same module.
why it matters
The predicate is invoked by the theorems alkali_halogen_ionic and alkali_halogen_stable_1_1 to prove that alkali-halogen pairs form stable 1:1 ionic compounds. It supplies the low-electronegativity donor required by the module's 8-tick closure drive and electronegativity-difference threshold. The list itself is reused from IonizationEnergy and MetallicBond, where it is justified by minimum ionization energy within each period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.