# The ionization and generalized ionization conjectures

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Generalized ionization energies for full Coulomb atoms](../../preprints/Generalized-ionization-energies-for-full-Coulomb-atoms-September-24-2026/paper.pdf)
- [Generalized outer-electron radii of neutral Coulomb atoms](../../preprints/Generalized-outer-electron-radii-of-neutral-Coulomb-atoms-September-24-2026/paper.pdf)

## Scope

The formalization gives the large-ionization asymptotics for the full nonrelativistic two-spin Coulomb atom. Let $I_m(Z)$ be the energy needed to remove $m$ electrons from a neutral atom of nuclear charge $Z$. There is a positive coefficient $a_{\mathrm{TF}}$ with the Thomas–Fermi variational characterization such that $I_m(Z)/m^{7/3}\to a_{\mathrm{TF}}$ whenever $m\to\infty$ and $Z/m\to\infty$, with integers $Z>m\ge1$. The corresponding iterated limsup and liminf limits hold with $Z\to\infty$ first. The energy uses the full antisymmetric Sobolev form domain; fixed-$m$ convergence and ground-state attainment are outside this statement.

For neutral Coulomb atoms with two electron spin states, the formalization proves the asymptotic law for generalized outer-electron radii defined by an expected exterior electron mass $m$. For every choice of normalized ground states, both the upper and lower large-nuclear-charge radius limits satisfy
$m^{1/3}R_m\longrightarrow (81\pi^2/2)^{1/3}$ as $m\to\infty$. The large-nuclear-charge limit is taken first. Ground states are inputs to the statement; their existence is not asserted separately.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Generalized Coulomb ionization-energy asymptotics | [CoulombIonization.lean](../ComparatorChallenges/CoulombIonization.lean) |
| Asymptotic outer-electron radii of neutral atoms | [CoulombRadii.lean](../ComparatorChallenges/CoulombRadii.lean) |