The ionization and generalized ionization conjectures

3 papersLean

For the full nonrelativistic Coulomb model with two electron spin states, proves that a molecule with M fixed nuclei of charges at least one and total charge Z strictly binds at most \(Z+CM\) electrons. Neutral-atom first ionization energies and radii containing all but an expected half-electron have universal positive upper and lower bounds. The energy cost of removing m electrons has Thomas–Fermi asymptotics as \(m\to\infty\) and \(Z/m\to\infty\); neutral-atom outer radii have the corresponding iterated-limit asymptotics, taking \(Z\to\infty\) first.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Uniform excess charge for Coulomb molecules and the outer radius of neutral atoms

OpenAI · September 24, 2026

We prove that a molecule with M fixed nuclei of real charges at least one and total nuclear charge Z strictly binds at most \(Z+CM\) electrons, where C is universal. The result holds for the full nonrelativistic Coulomb Hamiltonian with two spin states and arbitrary distinct nuclear positions. For neutral atoms with integer nuclear charge Z ≥ 1, the first ionization energy and, for every ground state, the radius outside which one half of an electron remains are each bounded above and below by positive universal constants.

Read PDF Download Source

Cite

@misc{OAI:Uniform-excess-charge-for-Coulomb-molecules-and-the-outer-radius-of-neutral-atoms-September-24-2026,
  author = {{OpenAI}},
  title = {{Uniform excess charge for Coulomb molecules and the outer radius of neutral atoms}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-excess-charge-for-Coulomb-molecules-and-the-outer-radius-of-neutral-atoms-September-24-2026/paper.pdf}{OAI:Uniform-excess-charge-for-Coulomb-molecules-and-the-outer-radius-of-neutral-atoms-September-24-2026}},
  year = {2026}
}

Generalized ionization energies for full Coulomb atoms

OpenAI · September 24, 2026

We prove the energy part of the generalized ionization conjecture for full nonrelativistic Coulomb atoms with two electron spin states. The energy needed to remove m electrons is asymptotic to \(a_{\mathrm{TF}}m^{7/3}\) whenever \(m\to\infty\) and \(Z/m\to\infty\), with the Thomas–Fermi constant in atomic units. We also obtain both conjectured iterated limits.

Read PDF Download Source

Cite

@misc{OAI:Generalized-ionization-energies-for-full-Coulomb-atoms-September-24-2026,
  author = {{OpenAI}},
  title = {{Generalized ionization energies for full Coulomb atoms}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Generalized-ionization-energies-for-full-Coulomb-atoms-September-24-2026/paper.pdf}{OAI:Generalized-ionization-energies-for-full-Coulomb-atoms-September-24-2026}},
  year = {2026}
}

Generalized outer-electron radii of neutral Coulomb atoms

OpenAI · September 24, 2026

We prove the radius part of the generalized ionization conjecture for neutral nonrelativistic Coulomb atoms with two spin states. For every choice of ground states, the upper and lower large-nuclear-charge limits of the radius defined by an expected exterior electron mass m are both asymptotic to \((81\pi^2/2)^{1/3}m^{-1/3}\) as m tends to infinity.

Read PDF Download Source

Cite

@misc{OAI:Generalized-outer-electron-radii-of-neutral-Coulomb-atoms-September-24-2026,
  author = {{OpenAI}},
  title = {{Generalized outer-electron radii of neutral Coulomb atoms}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Generalized-outer-electron-radii-of-neutral-Coulomb-atoms-September-24-2026/paper.pdf}{OAI:Generalized-outer-electron-radii-of-neutral-Coulomb-atoms-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

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
Asymptotic outer-electron radii of neutral atoms	CoulombRadii.lean

Scope note on GitHub →