Fatou's Conjecture

### What is the conjecture

Let $f: \mathbb{P}^1(\mathbb{C}) \to \mathbb{P}^1(\mathbb{C})$ be a rational map of degree $d \geq 2$ (where $\mathbb{P}^1(\mathbb{C})$ is the Riemann sphere). A critical point of $f$ is a point where the derivative vanishes. The conjecture states that for all rational maps, except postcritically finite maps and Lattés examples, every critical point tends to a periodic orbit under iteration. More precisely, for each critical point $c$ of $f$, the orbit $\{c, f(c), f^2(c), \ldots\}$ either converges to a periodic point or is eventually periodic, provided the map is not in one of the exceptional families.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Fatou_conjecture, https://press.princeton.edu/books/paperback/9780691002583/the-real-fatou-conjecture

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-01-22)

The Fatou conjecture involves complex dynamics of rational maps on the Riemann sphere, which requires substantial formalization infrastructure. While Mathlib has definitions of rational functions and basic complex analysis, it lacks dedicated theories for: (1) the Riemann sphere as a formal projective line, (2) iterative dynamics and periodic orbits for general maps, (3) critical points of rational maps and their dynamics, and (4) the classification of exceptional maps (postcritically finite and Lattés maps). The statement itself requires formalizing these core dynamical concepts, and the informal exceptions (special cases) would need precise mathematical characterization. Significant foundational work in dynamical systems theory would be needed.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-37
* ams-30

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

No repository files, tests, or entry points are named. Start by checking the cited Wikipedia article and Princeton source, then clarify precise definitions for rational-map dynamics, critical-point orbits, postcritically finite maps, and Lattés examples before attempting formalization. Done would be a precise Lean statement with the exceptional cases formally characterized.

Written by the indexing model from the issue text.