ionization_monotone_within_period
plain-language theorem explainer
The theorem establishes that the ionization proxy increases strictly with atomic number within a fixed period. Chemists modeling periodic trends or RS-based predictions of first ionization energies would cite this result. The proof reduces the claim to a direct comparison of valence electron counts via simplification and arithmetic.
Claim. For natural numbers $Z_1 < Z_2$ with $Z_1$ at or beyond its period start $C(Z_1)$ and $C(Z_1) = C(Z_2)$, the proxy satisfies $P(Z_1) < P(Z_2)$ where $P(Z) := Z - C(Z)$ and $C$ is the previous noble-gas closure.
background
The module derives first ionization energies from φ-ladder scaling. Ionization proxy equals valenceElectrons Z, defined as Z minus prevClosure Z (the atomic number of the preceding noble gas). The proxy runs from 1 for alkali metals to the period length for noble gases and captures the cost to break into a forming shell, per its definition.
proof idea
The tactic proof first applies simp to unfold ionizationProxy into valenceElectrons and then into Z minus prevClosure. It introduces Z2 >= prevClosure Z2 by omega and finishes with a direct omega comparison of the positions within the shared period.
why it matters
This result underpins the sawtooth pattern for ionization energies predicted by RS φ-ladder scaling in the module. It directly supports the predictions that alkali metals minimize and noble gases maximize ionization within each period. The declaration fills the P0-A2 claim and aligns with period-boundary enforcement from the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.