noble_max_ionization
plain-language theorem explainer
Noble gases attain the maximum ionization proxy value within each period, exactly equal to the period length. Researchers deriving ionization energies from the Recognition Science phi-ladder would reference this result to anchor the upper end of the sawtooth pattern. The proof is a one-line term reduction that unfolds the proxy definition and invokes the complete-shell theorem for noble gases.
Claim. If $Z$ is a noble gas, then the dimensionless ionization proxy of $Z$ equals the length of the period containing $Z$.
background
In the Recognition Science treatment of chemistry, ionization energy is modeled via a dimensionless proxy that tracks valence electron count within each period. The proxy runs from 1 for alkali metals to the full period length for noble gases, capturing the increasing cost to remove an electron as the shell fills. Period length is defined as the difference between consecutive shell closures. Noble gas membership is the predicate that $Z$ belongs to the list of shell-closure atomic numbers.
proof idea
The proof is a term-mode one-liner. It first simplifies the ionizationProxy definition, which reduces to valenceElectrons, then directly applies the noble_gas_complete_shell theorem to the hypothesis that $Z$ is a noble gas.
why it matters
This result establishes the upper bound of the ionization sawtooth within the RS chemistry model. It completes the prediction that noble gases exhibit maximum ionization energy per period, as stated in the module's key predictions. The placement follows from the periodic table structure imported from upstream, tying into the broader phi-ladder scaling for energies. It supports the falsification test on observed ordering within periods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.