isAlkaliMetal
plain-language theorem explainer
Elements with atomic number Z qualify as alkali metals exactly when valenceElectrons Z equals 1 and Z exceeds 1. Researchers deriving ionization energy orderings from φ-ladder scaling cite this predicate to identify the minimum per period. The definition is a direct conjunction that imports and applies the valence count from the periodic table module.
Claim. An element with atomic number $Z$ is an alkali metal if valenceElectrons$(Z) = 1$ and $Z > 1$.
background
The module predicts first ionization energies via φ-rail scaling: base energies grow as φ^{2n} for period n, with within-period position factors producing a sawtooth. Valence electrons count the electrons beyond the previous noble gas core, so noble gases occur precisely where this count equals the period length. The upstream valenceElectrons definition supplies this count as Z minus prevClosure Z; the alkali predicate simply isolates the valence-equals-1 case while excluding hydrogen.
proof idea
The definition is a direct conjunction of the imported valenceElectrons predicate equaling 1 with the inequality Z > 1. No lemmas or tactics are applied beyond the function application itself.
why it matters
This predicate supplies the alkali-metal hypothesis for the alkali_halogen_ionic and alkali_halogen_stable_1_1 theorems, which verify ionic bond formation and 1:1 compound stability. It realizes the module's central claim that alkali metals exhibit minimum ionization energy within each period under the φ-ladder sawtooth. The definition therefore anchors the chemical classification layer of the Recognition Science ionization model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.