## Motivation
The **spectral gap** of a quantum many-body Hamiltonian is the difference between the energy of its ground state and the energy of its first excited state, in the limit of infinitely many particles. Whether a given microscopic interaction produces a gapped or a gapless system decides much of the macroscopic physics: gapped systems have exponentially decaying correlations and well-defined quantum phases, gapless systems sit at critical points and can display algebraically decaying correlations. Several long-standing questions — the **Haldane conjecture** for antiferromagnetic spin chains, the existence of gapped topological spin liquids, and the **Yang–Mills mass gap** — are instances of the question "given the interaction, is the system gapped?".
Cubitt, Pérez-García and Wolf proved that this question, posed for families of two-dimensional translationally invariant nearest-neighbour spin models, admits no algorithmic answer: the **spectral gap problem is undecidable** ([Nature 528, 207–211 (2015)](https://doi.org/10.1038/nature16059); full version: [Forum of Mathematics, Pi 10:e14 (2022)](https://doi.org/10.1017/fmp.2021.15), also [arXiv:1502.04573](https://arxiv.org/abs/1502.04573)).
Timeline of the ingredients the proof rests on: Turing's undecidability of the halting problem (1936); Berger's undecidability of the domino problem (1966) and Robinson's aperiodic tile set ([Inventiones 12, 177–209 (1971)](https://doi.org/10.1007/BF01418780)); Feynman's and Kitaev's circuit-to-Hamiltonian constructions, which turn a computation into a ground state; Gottesman and Irani's translationally invariant one-dimensional Hamiltonians encoding computation ([FOCS 2009](https://arxiv.org/abs/0905.2419)); and Bitansky–Vadhan-style quantum Turing machine engineering from Bernstein and Vazirani ([SIAM J. Comput. 26, 1411–1473 (1997)](https://doi.org/10.1137/S0097539796300921)). The 2015 result was later sharpened to one-dimensional chains by Bausch, Cubitt, Lucia and Pérez-García ([PRX 10, 031038 (2020)](https://doi.org/10.1103/PhysRevX.10.031038)).
## Setting
Fix a local dimension $d$ and, for each side length $L$, the square lattice $\Lambda(L)=\{1,\dots,L\}^2$ with **open boundary conditions**. Each site carries a copy of $\mathbb{C}^d$, so the state space of the lattice has the standard product basis indexed by assignments of a level in $\{1,\dots,d\}$ to each site. A model is specified by three Hermitian matrices: an on-site term $h_1$ of size $d\times d$, and two interactions $h_{\mathrm{row}},h_{\mathrm{col}}$ of size $d^2\times d^2$ acting on horizontally and vertically adjacent pairs. The Hamiltonian of the finite lattice is
$$H^{\Lambda(L)} \;=\; \sum_{\text{horizontal edges}} h_{\mathrm{row}}^{(i,j)} \;+\; \sum_{\text{vertical edges}} h_{\mathrm{col}}^{(i,j)} \;+\; \sum_{k\in\Lambda(L)} h_1^{(k)},$$
the same three matrices being used at every edge and every site, which is what **translational invariance** means here. The quantity $\max\{\|h_1\|,\|h_{\mathrm{row}}\|,\|h_{\mathrm{col}}\|\}$ is the **local interaction strength**.
Write $\lambda_0(H^{\Lambda(L)})\le\lambda_1(H^{\Lambda(L)})\le\cdots$ for the eigenvalues and $\Delta(H^{\Lambda(L)})=\lambda_1-\lambda_0$ for the finite-size gap. The family $\{H^{\Lambda(L)}\}_L$ is
- **gapped** (Definition 1 of the source) if there are $\gamma>0$ and $L_0$ such that for all $L>L_0$ the ground state of $H^{\Lambda(L)}$ is non-degenerate and $\Delta(H^{\Lambda(L)})\ge\gamma$;
- **gapless** (Definition 2 of the source) if there is $c>0$ such that for every $\varepsilon>0$ there is an $L_0$ with: for all $L>L_0$, every point of $[\lambda_0,\lambda_0+c]$ lies within $\varepsilon$ of the spectrum of $H^{\Lambda(L)}$.
These two conditions are not negations of each other; the construction guarantees that every instance falls into one of them. The **ground state energy density** is $E_\rho=\lim_{L\to\infty}\lambda_0(H^{\Lambda(L)})/L^2$.
## Formalization targets
### Goal — Theorem 3 of the source
For a fixed universal machine and every $n$, one explicit family of interactions, built from fixed integer-valued matrices $A,A',B,C,D,D'$, a diagonal projector $\Pi$, a rational $\beta>0$ that may be taken arbitrarily small, and an algebraic $\alpha(n)\le 2\beta$,
$$h_1(n)=\alpha(n)\Pi,\qquad h_{\mathrm{col}}(n)=D+\beta D',$$
$$h_{\mathrm{row}}(n)=A+\beta\Bigl(A'+e^{i\pi\varphi}B+e^{-i\pi\varphi}B^{\dagger}+e^{i\pi 2^{-|\varphi|}}C+e^{-i\pi 2^{-|\varphi|}}C^{\dagger}\Bigr),$$
with $\varphi=\varphi(n)$ the rational whose binary expansion after the point is the binary expansion of $n$ reversed, satisfies: the local interaction strength is at most $1$; if the machine halts on input $n$ the family is gapped with gap at least $1$; and if it does not halt the family is gapless. Since halting is undecidable, no algorithm decides gappedness, even with the promise that exactly one of the two alternatives holds and even at fixed local dimension $d$.
### Milestones
The milestone list follows the numbering of the full version: Lemma 8 and Theorem 9 (reduction of halting to ground state energy and to arbitrary low-energy properties), Corollary 7 (the same undecidability for unconstrained local dimension, with rational interactions), Proposition 53 and Corollary 54 (the diverging ground state energy and its promise version), and Theorem 5 (undecidability of the ground state energy density).
## Significance
The result rules out a general algorithm — and therefore any complete general method — for deciding gappedness from the interaction matrices, however much computing power is available; the property genuinely depends on arbitrarily large system sizes. It also implies, via the standard link between undecidability and independence, that there are concrete finite-dimensional models whose gap is independent of the axioms of any consistent recursively axiomatized formal system (Corollary 4 of the source), and it transfers to other low-energy properties such as the existence of algebraically decaying ground-state correlations.
The theorem is proved; none of it is formalized. This mission produces the machine-checked version. The reusable infrastructure it forces into existence is substantial on its own: a formal model of translationally invariant lattice Hamiltonians and their thermodynamic-limit spectral behaviour, the tiling layer, and computational-history-state Hamiltonians. Each milestone is a self-contained statement that can be attacked without the others.
## Difficulty
The obvious approach — encode a halting computation as an energy penalty — gives the ground state *energy* of a finite lattice, not a property of the limit; this is exactly what Lemma 8 achieves, and it is not enough, because a gap is a statement about the sequence of spectra as $L\to\infty$ and is insensitive to any single lattice size. The construction must make the halting information visible at *all* sufficiently large sizes at once while a fixed finite local dimension carries every instance $n$. That forces three separate difficulties: an aperiodic (Robinson) tiling to create squares of every size $2^n$ inside one translationally invariant model; a quantum phase-estimation Turing machine whose transition amplitudes encode $n$ in a single phase $e^{i\pi\varphi(n)}$, so that the instance index does not inflate the local dimension; and a history-state Hamiltonian whose low-energy spectrum can be controlled well enough that a positive energy density in the halting case turns into a genuine spectral gap, and a vanishing one into a dense spectrum above the ground state.
## Formalization scope
The development commits to the following conventions, all of which are visible in the definition items of this mission.
1. Lattices are finite: sites are pairs of indices in $\{0,\dots,L-1\}$, edges are consecutive pairs within a row or a column (**open boundary conditions**; the periodic case of Section 6.3 of the source is out of scope).
2. Operators are complex matrices indexed by product-basis configurations; the interactions are embedded by acting as the given matrix on the two sites of an edge and as the identity elsewhere.
3. The spectrum is taken as the set of **real** numbers in the matrix spectrum, and $\lambda_0$ is its infimum; every statement carries the Hermiticity hypotheses that make this the usual spectrum. Multiplicities are dimensions of eigenspaces, which is how the "identity of spectra as multisets" of Theorem 9 is expressed.
4. Gapped, gapless and the energy density are properties of the whole family $\{H^{\Lambda(L)}\}_L$ generated by a fixed triple of matrices, exactly as in Definitions 1 and 2.
5. Operator norms are $\ell_2$ operator norms; the local interaction strength is the maximum of the three.
6. Machines are represented by partial recursive codes: "halts on input $n$" is definedness of the evaluation, and "has not halted after $L$ steps" is the step-bounded evaluation returning nothing. The explicit local-dimension bounds of Lemma 8 and Theorem 9, which are stated in the source in terms of the number of internal states and the alphabet size of a Turing machine, are replaced by the existence of a finite local dimension.
Degenerate readings are excluded: a zero local dimension satisfies none of the statements, since a non-degenerate ground state requires a one-dimensional eigenspace and the gapless condition requires a non-empty spectrum; and every existential statement fixes the matrices before quantifying over all instances $n$ and all lattice sizes $L$.
Contributions are welcome at any milestone, and also on the infrastructure the milestones need — Wang tilings and the Robinson tile set, Gottesman–Irani history-state Hamiltonians, and quantum Turing machines in the Bernstein–Vazirani sense — which are needed for Theorem 6 and Lemma 47 of the source and are not yet part of this mission's item list.
## Selected references
- T. S. Cubitt, D. Pérez-García, M. M. Wolf, *Undecidability of the Spectral Gap* (full version), Forum of Mathematics, Pi 10:e14, 1–102 (2022). https://doi.org/10.1017/fmp.2021.15 — the version all statements of this mission are formalized against; preprint: https://arxiv.org/abs/1502.04573
- T. S. Cubitt, D. Pérez-García, M. M. Wolf, *Undecidability of the spectral gap*, Nature 528, 207–211 (2015). https://doi.org/10.1038/nature16059
- R. M. Robinson, *Undecidability and nonperiodicity for tilings of the plane*, Inventiones Mathematicae 12, 177–209 (1971). https://doi.org/10.1007/BF01418780
- D. Gottesman, S. Irani, *The quantum and classical complexity of translationally invariant tiling and Hamiltonian problems*, FOCS 2009. https://arxiv.org/abs/0905.2419
- E. Bernstein, U. Vazirani, *Quantum complexity theory*, SIAM J. Comput. 26, 1411–1473 (1997). https://doi.org/10.1137/S0097539796300921
- J. Bausch, T. S. Cubitt, A. Lucia, D. Pérez-García, *Undecidability of the spectral gap in one dimension*, Phys. Rev. X 10, 031038 (2020). https://doi.org/10.1103/PhysRevX.10.031038
15 thms2 active usersReviewed
Captain: Lucas
Gribov Ambiguity: no continuous gauge fixing (Singer 1978)Research Paper
## Motivation
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a
gauge-invariant weight over the space $\mathfrak{A}$ of vector potentials (connections) of a
principal bundle. The integrand is constant on the orbits of the group $\mathcal{G}$ of gauge
transformations, so the integral over $\mathfrak{A}$ diverges and one is supposed to integrate
instead over the orbit space $\mathfrak{R} = \mathfrak{A}/\mathcal{G}$. The Faddeev–Popov
procedure realizes this by *fixing a gauge*: choosing, continuously in the orbit, exactly one
vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for $SU(2)$ potentials on
$\mathbb{R}^3$ (or $\mathbb{R}^4$) with suitable conditions at infinity, the Coulomb gauge
condition does not do this: the Coulomb slice through the zero potential meets the orbit of the
zero potential again, far from the origin. These extra intersections are the **Gribov copies**;
R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, *Some Remarks on the Gribov Ambiguity* (Commun. Math. Phys. **60** (1978) 7–12),
showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity
are those of Gribov — gauge transformations extending to the one-point compactification with
value $I$ at infinity, so that the base manifold is $M = S^3$ or $M = S^4$ — then **no**
continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space
of irreducible connections is weakly contractible, while the gauge group is not, and a
weakly contractible principal bundle admits no global continuous section.
## Setting
Fix $N \ge 2$ and take the structure group $SU(N)$, the group of $N \times N$ complex matrices
$U$ with $U^\ast U = I$ and $\det U = 1$, topologized as a subspace of matrices. Let
$S^r$ denote the unit sphere of $\mathbb{R}^{r+1}$, with base point $m$ the north pole.
For the trivial $SU(N)$-bundle over a space $M$, a gauge transformation is a map
$\varphi : M \to SU(N)$, and the **gauge group** is
$$\mathcal{G}(M,N) \;=\; C\bigl(M, SU(N)\bigr),$$
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects
matter. The **based gauge group** $\mathcal{G}_m = \{\varphi : \varphi(m) = I\}$ is the subgroup
of transformations that are the identity at the base point. The constant transformations with
value in the centre $Z_N = \{e^{2\pi i k/N} I\}$ of $SU(N)$ form a normal subgroup, and the
**reduced gauge group** is the quotient
$$\overline{\mathcal{G}}(M,N) \;=\; \mathcal{G}(M,N)/Z_N$$
with the quotient topology. The centre acts trivially on vector potentials, so
$\overline{\mathcal{G}}$ is the group that acts effectively.
A group $G$ acting continuously on a space $\mathfrak{A}$ has orbit space
$\mathfrak{A}/G$ with the quotient topology, and a **gauge fixing** is a continuous map
$s : \mathfrak{A}/G \to \mathfrak{A}$ with $p \circ s = \mathrm{id}$, where
$p : \mathfrak{A} \to \mathfrak{A}/G$ is the projection: a continuous choice of exactly one point
on each orbit. The action is **principal** when it is free and the division map, which sends a
pair of points on one orbit to a group element carrying the second to the first, can be chosen
continuously; this is the topological content of "$p$ is a principal $G$-bundle". The space
$\mathfrak{A}$ is **weakly contractible** when it is nonempty and all its homotopy groups vanish.
In the paper, $\mathfrak{A}$ is the affine space of connections, $\mathfrak{R}$ its set of
irreducible members, and Theorems 1 and 2 say exactly that $\mathfrak{R}$ is a weakly
contractible principal $\overline{\mathcal{G}}$-space.
## Formalization targets
### Goal — Corollary 4 (no gauge fixing)
For $r \in \{3,4\}$, $N \ge 2$, and every weakly contractible principal
$\overline{\mathcal{G}}(S^r,N)$-space $A$:
$$\nexists\, s : A/\overline{\mathcal{G}}(S^r,N) \longrightarrow A \quad\text{continuous with}\quad p \circ s = \mathrm{id}.$$
By Theorems 1 and 2 of the paper the space of irreducible connections over $S^3$ or $S^4$ is such
an $A$, so the goal contains Singer's Corollary 4 for that space; it leaves the analytic
construction of the space of connections unfixed, which is what makes it statable today.
### Milestone level — Theorem 3
$$\exists\, j \ge 1: \quad \pi_j\bigl(\overline{\mathcal{G}}(S^r,N)\bigr) \neq 0, \qquad r \in \{3,4\},\ N \ge 2 .$$
### Milestone level — Theorem 5 and its homotopy inputs
$$\pi_j\bigl(\mathcal{G}_m(S^r,N)\bigr) \;\cong\; \pi_{j+r}\bigl(SU(N)\bigr), \qquad
\pi_3(SU(N)) \cong \mathbb{Z}, \qquad \pi_4(SU(N)) = 0 \ (N\ge 3), \qquad \pi_4(SU(2)) \cong \mathbb{Z}/2 .$$
## Significance
The result rules out the existence of a global gauge in the topological sense: every gauge
condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be
read as a local statement, patched with a partition of unity over the orbit space (as the last
section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be
repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction
of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than
it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks:
homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for
$0 \to \mathcal{G}_m \to \mathcal{G} \to SU(N) \to 0$, and the classical computations
$\pi_3(SU(N)) \cong \mathbb{Z}$, $\pi_4(SU(N)) = 0$ for $N \ge 3$, $\pi_4(SU(2)) \cong \mathbb{Z}/2$.
Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned
revision contains homotopy groups as a definition together with their group structure, but
essentially no computation of them.
## Difficulty
The naive approach to the goal — build a section by hand, or average over the group — fails
because $\overline{\mathcal{G}}$ is neither compact nor contractible and the obstruction is
global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no
local argument can produce a contradiction. The proof has to convert a section into a
homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the
group as a retract of the total space, so all homotopy groups of the group would vanish; the work
is then to show that some homotopy group of the reduced gauge group does not vanish, which needs
the identification of the based gauge group with a mapping space, the exact sequences relating
$\mathcal{G}_m$, $\mathcal{G}$ and $\overline{\mathcal{G}}$, and non-trivial homotopy groups of
$SU(N)$ — including $\pi_6(S^3) \cong \mathbb{Z}/12$ for the $SU(2)$ case of Theorem 3.
## Formalization scope
The formalization commits to the following conventions, all of them visible in the definitions of
this mission.
- The bundle is the **trivial** $SU(N)$-bundle, so gauge transformations are literally maps
$M \to SU(N)$. This is the case of Gribov's original setting over $S^3$; over $S^4$ the paper
also treats bundles of nonzero Pontrjagin index, which are out of scope here.
- Gauge transformations are **continuous**, not smooth, with the compact-open topology; Singer's
Theorem 5 uses smoothing homotopies to pass between the two, and the homotopy-theoretic content
is the same.
- $SU(N)$ is the special unitary group of complex $N \times N$ matrices, with its subspace
topology; $S^r$ is the unit sphere of $\mathbb{R}^{r+1}$ with its subspace topology.
- Homotopy groups are Mathlib's `HomotopyGroup`, based at the identity element.
- The **space of connections is not constructed**: Mathlib has no space of connections on a
principal bundle, and building one is a mission of its own. The goal therefore quantifies over
an arbitrary topological space carrying a weakly contractible principal action of the reduced
gauge group — exactly the properties Theorems 1 and 2 establish for the irreducible
connections.
- This quantification is not vacuous: such spaces exist (the total space of a universal
$\overline{\mathcal{G}}$-bundle is one), so the goal is a genuine non-existence statement and
not a statement about an empty class. Conversely it is not trivially true: the hypotheses do
not mention any homotopy invariant of the gauge group, and refuting a section requires
Theorem 3.
- The paper's analytic statements — Theorem 1 (openness and density of the irreducible
connections, principal bundle structure), Theorem 2 (weak contractibility), Theorem 6
($\pi_1$ of the irreducible orbit space), Theorem 7 (no flat connection), Theorem 8 (tangency
of orbits to the Coulomb slice) and Theorem 9 (the canonical connection and its curvature) —
are out of scope until a space of connections exists in Lean. Contributions that build one, in
reusable form, are welcome and would let this mission be extended to them.
## Selected references
- V. N. Gribov, *Instability of non-abelian gauge theories and impossibility of choice of Coulomb
gauge*, SLAC Translation 176 (1977); Nucl. Phys. B **139** (1978) 1–19,
[doi:10.1016/0550-3213(78)90175-X](https://doi.org/10.1016/0550-3213(78)90175-X).
- I. M. Singer, *Some Remarks on the Gribov Ambiguity*, Commun. Math. Phys. **60** (1978) 7–12,
[doi:10.1007/BF01609471](https://doi.org/10.1007/BF01609471).
- R. Jackiw, I. Muzinich, C. Rebbi, *Coulomb gauge description of large Yang-Mills fields*,
Phys. Rev. D **17** (1978) 1576, [doi:10.1103/PhysRevD.17.1576](https://doi.org/10.1103/PhysRevD.17.1576).
- H. Toda, *Composition methods in homotopy groups of spheres*, Annals of Mathematics Studies 49,
Princeton University Press (1962).
8 thms1 active userReviewed
Captain: Yivy Yu
Birkhoff's Retrograde Global-Section Conjecture in the Planar Circular Restricted Three-Body ProblemOpen Problem
## Motivation and historical timeline
In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit ([Birkhoff 1915](https://doi.org/10.1007/BF03015982); [Liu--Salomão, Section 1.4](https://arxiv.org/abs/2506.17867v2)). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics ([Joung--van Koert, Introduction](https://arxiv.org/abs/2407.19159v3)).
In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 ([Joung--van Koert, Theorem 1.3](https://arxiv.org/abs/2407.19159v3); [Hryniewicz](https://arxiv.org/abs/0812.4076v8)). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for \(0\leq\mu\leq 1/2\) and \(2.1\leq c\leq 2.1+10^{-6}\) ([Theorems 1.2 and 1.5](https://arxiv.org/abs/2407.19159v3)). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to \(1/2\), in fact obtaining rational open books bound by every retrograde orbit in that regime ([Theorem 1.16](https://arxiv.org/abs/2506.17867v2)). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem ([Liu--Salomão 2026](https://arxiv.org/abs/2606.12912)). These results leave the universal finite-mass, all-subcritical statement below as the open target.
## Setting
Two primaries of masses \(1-\mu\) and \(\mu\), with \(0<\mu<1\), are fixed in rotating coordinates at \((-\mu,0)\) and \((1-\mu,0)\). For a massless particle with phase coordinates \((q_1,q_2,p_1,p_2)\), the Hamiltonian is
$$
H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1
-\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}}
-\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.
$$
This is equation (1.1) of [Joung--van Koert](https://arxiv.org/abs/2407.19159v3). Let \(h_1(\mu)=H_\mu(L_1)\) be the smallest collision-free critical value, where \(L_1\) lies between the primaries. The subcritical range is \(H_\mu=-c<h_1(\mu)\); there are then two bounded physical components, one around each primary ([Liu--Salomão, Section 4](https://arxiv.org/abs/2506.17867v2)).
The mission labels the primary at \((-\mu,0)\). With complex Levi-Civita variables \(z=z_1+iz_2\) and \(w=w_1+iw_2\), the inverse position map is \(q+\mu=2z^2\), and the regularized Hamiltonian is
$$
\begin{aligned}
K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2}
+2|z|^2(z_1w_2-z_2w_1)\\
&-\mu(z_1w_2+z_2w_1)
-\frac{\mu|z|^2}{|2z^2-1|}.
\end{aligned}
$$
On the collision-free domain, \(K_{\mu,c}=|z|^2(H_\mu+c)\), and its zero level regularizes collision with the labeled primary ([Joung--van Koert, equation (2.2)](https://arxiv.org/abs/2407.19159v3)). The selected component \(\Sigma_{\mu,c}\) is anchored at \((z,w)=(0,\sqrt{1-\mu})\). Below \(h_1\), it is a star-shaped three-sphere, invariant under the free antipodal deck map \((z,w)\mapsto(-z,-w)\), and it double-covers the corresponding Moser-regularized \(\mathbb{R}P^3\) component ([Joung--van Koert, Proposition 2.4](https://arxiv.org/abs/2407.19159v3)).
## Target
For every \(0<\mu<1\), every \(-c<h_1(\mu)\), and every complete flow \(\varphi\) on \(\Sigma_{\mu,c}\) generated by \(X_{K_{\mu,c}}\) and commuting with the antipodal map, prove
$$
\exists\,\delta\quad
\operatorname{GeometricRetrograde}(\delta)\ \land\
\operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).
$$
Here \(\delta\) consists of \(x\in\Sigma_{\mu,c}\) and a quotient period \(P>0\) with \(\varphi_P(x)=-x\), with no earlier positive time reaching either \(x\) or \(-x\). Its physical projection is required to be a \(q_2\)-symmetric, simple, collision-free loop of winding \(+1\) around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in [Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3](https://arxiv.org/abs/2407.19159v3).
The rational page is encoded by a smooth immersive disk lift \(\widetilde f:D^2\to\Sigma_{\mu,c}\). Its lift is embedded, its interior is transverse to \(X_{K_{\mu,c}}\), and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section ([Hryniewicz, Definition 1.1](https://arxiv.org/abs/0812.4076v8)).
## Significance
A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences ([Birkhoff 1915](https://doi.org/10.1007/BF03015982); [Joung--van Koert, Introduction](https://arxiv.org/abs/2407.19159v3)). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.
## Difficulty
Existence of a \(q_2\)-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every \(0<\mu<1\) and every energy below \(L_1(\mu)\) ([Liu--Salomão, Theorem 5.1](https://arxiv.org/abs/2506.17867v2)). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges ([Joung--van Koert, Theorem 1.5](https://arxiv.org/abs/2407.19159v3); [Liu--Salomão, Theorem 1.16](https://arxiv.org/abs/2506.17867v2)).
## Formalization scope
The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual `Flow` together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.
The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.
All theorem rows are Lean declarations ending in `by sorry`. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.
## Selected references
- G. D. Birkhoff, *The restricted problem of three bodies*, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. [DOI](https://doi.org/10.1007/BF03015982).
- U. Hryniewicz, *Fast finite-energy planes in symplectizations and applications*, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. [arXiv:0812.4076v8](https://arxiv.org/abs/0812.4076v8).
- C. Joung and O. van Koert, *Computational symplectic topology and symmetric orbits in the restricted three-body problem*, Nonlinearity 38 (2025), 025015. [arXiv:2407.19159v3](https://arxiv.org/abs/2407.19159v3).
- L. Liu and P. A. S. Salomão, *Finite energy foliations and global dynamics in the restricted three-body problem*, arXiv:2506.17867v2 (25 May 2026). [Preprint](https://arxiv.org/abs/2506.17867v2).
- L. Liu and P. A. S. Salomão, *Birkhoff conjecture and finite energy foliations in Hill's lunar problem*, arXiv:2606.12912 (2026). [Preprint](https://arxiv.org/abs/2606.12912).