Papers With

← All papers
First page of When do all iterates of $x^2 + a$ have maximal Galois group?

When do all iterates of $x^2 + a$ have maximal Galois group?

Michael Stoll

math.NT Nov 10, 2026 · v1
formalization mathlib number-theory algebra
Read PDF arXiv abstract Code
TL;DR
The paper's main results on surjectivity of arboreal Galois representations for x^2+a are formalized in Lean with Mathlib, with a blueprint on GitHub.
Abstract
We provide an (in our opinion) simpler proof of the main results of [Stoll1992,Li2020,Li2021] on the question for which integers $a$ the Galois groups of all iterates of $x^2 + a$ are maximal (equivalently, the associated arboreal Galois representation is surjective). At the same time, we extend the results to rational parameters $a$. The main result states that for a subset of rational numbers of relative density $1/2$ in the complement of a certain open interval, the maximality of the Galois group of the second iterate is sufficient for the arboreal Galois representation to be surjective. We also discuss experimental evidence suggesting that a similar statement involving the fourth iterate may hold in general. The results were obtained in collaboration with Claude (Anthropic's AI model); they are also formalized in Lean (except for the experimental evidence).
Problem

The question is for which rational a the Galois groups of all iterates of x^2 + a are maximal, i.e. when the associated arboreal Galois representation is surjective. Earlier results of Stoll and Li covered only integer a.

Approach

Surjectivity is reduced to 2-independence of the sequence c_n modulo squares. This independence is detected using quadratic characters on Q^× (sign, valuations, Legendre symbols, and the characters mod 4 and mod 8), combined with sign information on c_n and congruence conditions on a = r/s. The results were developed in collaboration with Claude and formalized in Lean/Mathlib, with a blueprint. Computational experiments test a conjecture involving the fourth iterate.

Results

For a set of rationals of relative density 1/2 outside an open interval (-2, α), maximality of the Galois group of the second iterate implies surjectivity of the full representation. This recovers and extends the integer case to rational a. Computations up to height 10^6 show that surjectivity at level 3 implies surjectivity at level 20, except for a = 2/3 and a = -6/7.