sawtooth_reset
plain-language theorem explainer
The theorem shows that the ionization proxy drops strictly after each noble gas closure: the alkali metal immediately following a noble gas has lower proxy value than the noble gas itself. Recognition Science derivations of periodic trends and chemists checking sawtooth ordering in first ionization energies would cite this result. The proof exhausts the six noble gas cases via membership elimination, substitutes the successor relation, and decides each inequality by native computation.
Claim. Let $Z_n$ be a noble gas atomic number and let $Z_a = Z_n + 1$ with $Z_a ≤ 118$. Then the period-position ionization proxy of $Z_a$ is strictly smaller than the proxy of $Z_n$.
background
The module derives first ionization energies from φ-ladder scaling. IonizationProxy(Z) equals valenceElectrons(Z) and runs from 1 for alkali metals to the period length for noble gases, capturing shell-closure cost. NobleGasZ lists the closure points [2,10,18,36,54,86] and isNobleGas asserts membership in that list. The upstream period definition supplies the φ^k scaling that sets the base energy per period, while the module doc states that alkali metals achieve minimum and noble gases maximum ionization within each period.
proof idea
The term proof unfolds isNobleGas and nobleGasZ, simplifies the membership disjunction, then performs exhaustive case split on the six possible noble-gas values. For each case it substitutes the successor hypothesis and invokes native_decide to confirm the strict inequality on the proxy values.
why it matters
The result closes the sawtooth-reset step required by the φ-ladder model in IonizationEnergy. It directly supports the module's key prediction that ordering (alkali minimum, noble maximum) emerges without data fitting and supplies one of the four explicit falsification criteria listed in the module. Within the Recognition framework it instantiates the position-factor component of the chemistry scaling that follows from T5 J-uniqueness and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.