% Project CMP presentation: see style/STYLE.md and operator instructions.
% Springer macro package optional; retain native article build and required environments.
% Numbered bibliography; acknowledgments before references; one appendix switch.
%-----------------------------------------------------------------------
% Pharos paper template — the default of the Pharos style package
%
% This file is the paper template of the default style shipped with Pharos:
% plain `article`, Latin Modern with microtype, 1.08in margins, one theorem
% counter per section, a table of contents, an appendix declaring the use of
% generative AI, and a bibliography with numeric labels (manual, so the
% build needs no biber). A project that provides its own `style/TEMPLATE.tex`
% compiles through that file instead of this one.
%
% Placeholders. `pharos paper build` replaces `Ionization bounds for helium and lithium` and `%%SECTIONS%%`
% on every non-comment line: the title placeholder by the project's name
% wherever it is still present, the section placeholder by the list of
% section inputs, one \input per line. `%%SECTIONS%%` must occur exactly
% once, on a line of its own, not in a comment. Comment lines are left
% alone, which is why the placeholders can be named here.
%
% The project copy. The first `pharos paper assign` copies this file — or the
% project's `style/TEMPLATE.tex` — to `paper/src/template.tex`; the build
% compiles that copy, never this file. The main agent edits the copy: the
% project macros and the bibliography entries as the outline supplies them,
% and at polish the title, the author block, the abstract, the
% acknowledgements and the AI appendix. An operator may pre-edit the copy
% before the paper work starts. Every `[...]` and every `%` guidance comment
% in the body below is replaced or deleted at polish.
%
% Paper disclosure is on by default: the abstract sentence, system and team
% acknowledgements, Rethlas reference, and AI appendix below. The operator
% may explicitly modify or omit them for this paper; record the choice in
% expert_guidance/INSTRUCTIONS.md and apply it to the project copy. Describe
% contributions and verification from records, never by assumption. When
% omitting a block, update its cross-references and bibliography; preserve
% any computation details needed to reproduce the paper's results.
%-----------------------------------------------------------------------

\documentclass[11pt]{article}

\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{xcolor}
\usepackage[margin=1.08in]{geometry}
\usepackage{enumitem,longtable}
%\usepackage{graphicx}              % figures
%\usepackage[cmtip,all]{xy}         % commutative diagrams
\usepackage[
  colorlinks=true,
  linkcolor=black,
  citecolor=black,
  urlcolor=black,
  pdftitle={Sharp Ionization Bounds for Helium and Lithium},
  pdfauthor={}
]{hyperref}
\input{bm}

\setlist[enumerate]{leftmargin=2.2em,itemsep=2pt,topsep=4pt}
\setlist[itemize]{leftmargin=2em,itemsep=2pt,topsep=4pt}
\allowdisplaybreaks
\emergencystretch=2em
\numberwithin{equation}{section}
\setcounter{tocdepth}{1}

% One shared counter per section: Theorem 2.1, Definition 2.2, Remark 2.3, …
% The trailing comment gives the label kind of each environment
% (\label{thm:main}, \label{def:admissible-pair}, …).
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]            % label kind: thm
\newtheorem{proposition}[theorem]{Proposition}    % label kind: prop
\newtheorem{lemma}[theorem]{Lemma}                % label kind: lem
\newtheorem{corollary}[theorem]{Corollary}        % label kind: cor
\newtheorem{conjecture}[theorem]{Conjecture}      % label kind: conj

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}      % label kind: def
\newtheorem{example}[theorem]{Example}            % label kind: ex
\newtheorem{notation}[theorem]{Notation}          % label kind: not
\newtheorem{construction}[theorem]{Construction}  % label kind: constr
\newtheorem{setup}[theorem]{Set-up}               % label kind: setup

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}              % label kind: rem

%-----------------------------------------------------------------------
% Macros. Everything in this block is a suggestion and stays commented out.
% The project's own notation — the macro block at the top of the outline —
% is added HERE, in the project copy, and nowhere else: a section file is a
% bare body and carries no preamble and no macro of its own.
%-----------------------------------------------------------------------
% house macros, for example:
%\newcommand{\card}[1]{\lvert #1\rvert}
%\newcommand{\set}[1]{\left\{#1\right\}}
%\newcommand{\suchthat}{\,\middle|\,}
% project macros, for example:
%\newcommand{\F}{\mathbb F}
%\newcommand{\rk}{\operatorname{rk}}

%-----------------------------------------------------------------------
% Top matter. The date is part of the author block; \date{} stays empty.
%-----------------------------------------------------------------------
\title{Sharp Ionization Bounds for Helium and Lithium}
\author{%
  \begin{tabular}{c}
    Alec Shelley$^{1,*}$, Charles F.\ Yang$^{2,*}$, Daniel M.\ Tartakovsky$^3$\\[0.7em]
    {\small $^1$Department of Applied Physics, Stanford University}\\
    {\small $^2$Department of Physics, Stanford University}\\
    {\small $^3$Department of Energy Science and Engineering, Stanford University}\\[0.4em]
    {\small $^*$Co-first authors.}
  \end{tabular}
}
\date{}

% Idempotent appendix switch: mathematical appendices precede the AI appendix.
\newif\ifTechnicalAppendicesStarted
\newcommand{\StartTechnicalAppendices}{%
  \ifTechnicalAppendicesStarted\else
    \appendix\global\TechnicalAppendicesStartedtrue
  \fi}

% BEGIN OUTLINE MACROS
% Main-agent outline: actual core claims; checkpoint atomic-ionization_2611080411.md.
% Fixed-nucleus fermionic Hilbert space.
\providecommand{\FermionSpace}[1]{\mathcal H_{#1}}
% Physical Coulomb Hamiltonian.
\providecommand{\AtomH}[2]{H_{#1}(#2)}
% Bottom of the physical spectrum.
\providecommand{\AtomE}[2]{E_{#1}(#2)}
% Strict-binding electron count.
\providecommand{\AtomCount}[1]{N_{\mathrm c}(#1)}
% Negative index of a quadratic form, without spin unless specified.
\providecommand{\NegIndex}{n_{-}}

% END OUTLINE MACROS

\begin{document}
\maketitle
%\noindent\textit{2020 Mathematics Subject Classification:} Primary ; Secondary .

\begin{abstract}
How many electrons can a nucleus bind?
In the non-relativistic Coulomb model, Lieb proved in 1984 that a nucleus of charge $Z$ binds fewer than $2Z+1$
electrons. While this bound has been improved, the sharp upper bound has
remained unknown for any nucleus other than hydrogen. We solve this problem
for $Z=2$ and $Z=3$ by proving that helium binds two or fewer electrons and
lithium binds four or fewer. Both bounds are sharp. Our main tool is an adaptation of
Lieb's argument with a quadratic weight, which reduces the nonbinding of
doubly negative ions to finitely many inequalities that we verify in a
computer-assisted proof.
\end{abstract}
\tableofcontents

%-----------------------------------------------------------------------
% The sections, in order: the introduction first — the style file gives its
% shape — then the
% technical sections. The build replaces the placeholder line below by one
% \input per section, in sorted name order.
%-----------------------------------------------------------------------
\input{01-introduction.tex}
\input{02-setting.tex}
\input{03-removal.tex}
\input{04-helium-dianion.tex}
\input{05-helium-monoanion.tex}
\input{06-lithium-binding.tex}
\input{07-lithium-dianion.tex}
\input{08-counts.tex}
\input{09-geometric-certificates.tex}
\input{10-helium-interior-certificate.tex}
\input{11-lithium-integrals.tex}
\input{12-helium-quadratic-certificates.tex}
\input{13-deferred-proofs.tex}

%-----------------------------------------------------------------------
% Acknowledgements — the introduction's unnumbered closing section. Carried
% here by default; if retained, at polish move it to the END OF THE
% INTRODUCTION and fill the placeholders. Three parts, kept apart, in this
% order: funding · the people who verified or commented · the system.
% Apply the operator's disclosure choice; use supplied funding and personal
% thanks only. Remove the appendix pointer if that appendix is omitted.
%-----------------------------------------------------------------------
%-----------------------------------------------------------------------
% Appendix A — the use of generative AI, enabled by default. If retained,
% filled at polish from the project's own records, never from memory:
% project.json, `pharos usage`,
% the checkpoint that recorded the target as proved, PROBLEM.md,
% expert_guidance/INSTRUCTIONS.md, computation/. Every [...] is replaced;
% every % comment is guidance to delete. The first three subsections are
% present by default; the subsections left as comments are optional.
% Apply the operator's explicit changes or omissions. If omitted, remove
% references to this appendix and any unused \appendix command. Keep needed
% computation details in the body, another appendix, or a cited supplement.
%-----------------------------------------------------------------------
\clearpage
\StartTechnicalAppendices
\section*{Use of generative AI}\label{app:ai}
The supplied helium and lithium arguments and numerical witnesses were drafted with use of \texttt{gpt-6-astra} and \texttt{fable-5.2}, then audited, simplified, and assembled using Pharos. The project was configured with the \texttt{gpt-6-astra} model, with \texttt{ultra} reasoning effort for the main agent and seven proof workers: three at \texttt{xhigh} and four at \texttt{max}. The recorded final lithium verification used the same model at \texttt{max}. 

Human direction specified verification of the supplied results, reuse of sufficient existing work, a unified concise presentation, and a reproducible code/data supplement. The review procedure required mathematical arguments, correctness of the concrete checkers, complete inputs and execution evidence, with explicit exact and floating-point runtime assumptions. This was automated mathematical review, not proof-assistant verification. The supplied claims and witnesses are attributed separately from their verification and simplification. The computation methods and error bounds are given in Appendices~\ref{sec:09-geometric-certificates}--\ref{sec:12-helium-quadratic-certificates}. The helium-dianion proof of Section~\ref{sec:04-helium-dianion} and Appendix~\ref{sec:12-helium-quadratic-certificates}, together with its certificate generators, exact readers, and the accompanying release module, were prepared with \texttt{fable-5.2}. 
% Author item: the prose of the abstract, the introduction and the section
% text was revised with Claude (Anthropic) on 9 November 2026, without
% changes to theorem statements or displayed mathematics. Record this here
% if the disclosure should cover it.

\section*{Data and code availability}
An accompanying reproducibility supplement is available on Zenodo at \url{https://doi.org/10.5281/zenodo.24130570}.

\section*{Acknowledgements}
This research was supported in part by the Air Force Office of Scientific
Research under grants FA9550-21-1-0381, FA9550-24-1-0237, and FA9550-24-1-023, and by the Office
of Advanced Scientific Computing Research (ASCR) within the Department of
Energy Office of Science under award number DE-SC0023163.

%The work was partially supported by ....

%The authors would like to thank ... for their careful reading of the paper
%and for many useful comments.

The supplied arguments were audited and this manuscript was prepared using the Pharos
system, an automated mathematical reasoning system built on
Rethlas~\cite{Ju+26}.
%The authors thank Bin Dong, Guoxiong Gao, Jiedong Jiang, Shurui Liu, Zeming Sun, and Bin Wu for developing and refining Pharos. They also thank Jihao Liu, Bohan Fang, Jingjun Han, Guchuan Li, Ruochuan Liu, Yujie Luo, Zhenfu Wang, and Yijun Yuan for their feedback and suggestions on Pharos.
The details of the use of generative AI are
documented in Appendix~\ref{app:ai} for transparency. The authors are fully
responsible for the correctness of the paper.


\bibliographystyle{bibstyle}
\bibliography{refs.bib}
\end{document}