Lemma 4.8 — the Julia set of a rational map of degree $\ge 2$ is nonempty

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements of this proposal, with full knowledge of the intended meaning and of the source. It was not produced by an independent, blind auditor, so it must not be treated as independent testimony: please compare the Lean code itself against the source.

Here a rational map $f$ is a pair of complex polynomials $(p,q)$ with $q\neq 0$ and $p,q$ coprime (in the sense $ap+bq=1$ for some polynomials $a,b$). Its degree is $\deg f=\max(\deg p,\deg q)$ (natural-number degrees, with $\deg 0=0$). It acts on $\hat{\mathbb C}=\mathbb C\cup\{\infty\}$ (the one-point compactification of $\mathbb C$) by: for finite $z$, $f(z)=\infty$ if $q(z)=0$ and $f(z)=p(z)/q(z)$ otherwise; and $f(\infty)=\infty$ if $\deg q<\deg p$, otherwise $f(\infty)=c/\operatorname{lc}(q)$ where $c$ is the coefficient of $p$ in degree $\deg q$ and $\operatorname{lc}(q)$ the leading coefficient of $q$ (so $f(\infty)=0$ when $\deg p<\deg q$). For a map $g:\hat{\mathbb C}\to\hat{\mathbb C}$, a point $z_0$ is in the Fatou set $F(g)$ iff there is an open set $V\subseteq\mathbb C$ containing the chart coordinate of $z_0$ (the point itself if $z_0$ is finite; $0$ if $z_0=\infty$) such that the family of maps $V\to\hat{\mathbb C}$, $w\mapsto g^{n}(\phi(w))$ ($n\ge 0$), with $\phi(w)=w$ in the finite case and $\phi(w)=1/w$ ($\phi(0)=\infty$) in the case $z_0=\infty$, is normal on $V$: every sequence from the family has a subsequence converging, uniformly on every compact subset of $V$ with respect to the chordal metric of $\hat{\mathbb C}$, to some map continuous on $V$. The Julia set is $J(g)=\hat{\mathbb C}\setminus F(g)$.

Statement. For every rational map $f$ with $\deg f=\max(\deg p,\deg q)\ge 2$, there exists a point $z\in\hat{\mathbb C}$ with $z\in J(f)$, i.e. $z$ is not in the Fatou set of the self-map $f$ of $\hat{\mathbb C}$.