alkali_min_ionization
plain-language theorem explainer
For natural numbers Z greater than 2 whose valence electron count equals 1, the ionization proxy equals 1. Modelers of periodic trends in Recognition Science cite this to fix the lower bound of the sawtooth ionization pattern forced by phi-ladder scaling. The proof is a one-line simplification that substitutes the definition of the proxy and matches the supplied hypothesis.
Claim. For any natural number $Z > 2$ with valence electrons of $Z$ equal to 1, the dimensionless ionization proxy of $Z$ equals 1.
background
The module derives first ionization energies from phi-rail scaling: base energy grows as phi to the power of twice the period index, with position within the period supplying a multiplicative factor that rises toward shell closure. Valence electrons for atomic number Z are defined as Z minus the atomic number of the preceding noble-gas closure; this count equals the period length precisely at noble gases. The ionization proxy is defined directly as this valence count, so it runs from 1 at alkali metals to the full period length at noble gases.
proof idea
The term proof applies simp only on the definition of ionizationProxy, which unfolds to valenceElectrons Z, then matches the hypothesis that this value equals 1.
why it matters
This theorem supplies the minimum vertex of the sawtooth ionization pattern required by the phi-ladder model in the module. It directly implements the key prediction that alkali metals exhibit minimum ionization energy per period, enabling the falsification test stated in the module documentation. No downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.