Local Connectivity of the Mandelbrot Set (MLC)Open Problem
## The set
For a complex parameter $c$, iterate the quadratic map
$$f_c(z) = z^2 + c$$
starting at the critical point $z = 0$. The **Mandelbrot set** is the set of parameters for which this orbit stays bounded:
$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$
Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.
$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism
$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$
between the complement of $M$ and the exterior of the closed unit disk.
## The question
**MLC conjecture.** *$M$ is locally connected*: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.
By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the *pinched disk* model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the **density of hyperbolicity** in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and **zero area for $\partial M$**.
MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.
## Timeline
- **1982** -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
- **1984/85** -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
- **1990** -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
- **1997** -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
- **1997** -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the *real* quadratic family.
- **1998** -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive *area* remains open.
- **2005** -- Buff and Cheritat construct quadratic *Julia* sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
- **Today** -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.
## What this mission asks for
The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".
The milestones are of three kinds, and are ordered accordingly:
1. **Foundations provable today** -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. **Known theorems from the literature** -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. **The open companions** -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.
All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.
16 thms4 active usersReviewed
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).