alkaliMetalZ
plain-language theorem explainer
AlkaliMetalZ enumerates the atomic numbers of the six alkali metals as the list [3, 11, 19, 37, 55, 87]. Modelers of ionization energies under Recognition Science phi-ladder scaling cite this fixed set to mark the minimum-energy positions within each period. The declaration is introduced by direct enumeration with no computation or external data.
Claim. Let $A = [3, 11, 19, 37, 55, 87]$ be the ordered list of atomic numbers for the alkali metals (Li, Na, K, Rb, Cs, Fr).
background
The module derives first ionization energy from phi-ladder scaling: base energy grows as phi to the power of twice the period index, with an additional position factor that increases energy toward period closure and fixed offsets for s/p/d/f blocks. Alkali metals occupy the valence-one starting position of each period and therefore carry the minimum ionization proxy. The upstream period definition supplies the scaling base as phi raised to k.
proof idea
Direct definition that binds the identifier to the explicit list of six natural numbers.
why it matters
The definition supplies the concrete input for isAlkaliMetal and for theorems such as alkali_halogen_ionic and alkali_low_ionization that verify the predicted minimum ionization per period. It realizes the sawtooth pattern and the falsification criterion stated in the module documentation: if the ordering alkali less than other elements less than noble fails on a pre-registered set, the phi-ladder model is refuted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.