Irreducibility of the iterates over ℚ #
An even polynomial in ℚ[X] that is reducible but has no nontrivial even divisor factors as
g · g(-X) (even_reducible_factorization); applied to f_n, this shows that a factorization of
f_n would make c_n a square (Lemma 1.2, irreducible_iteratedPoly_of_not_isSquare_cSeq). Since
no c_n is a square when -a is not one, every f_n is irreducible (Corollary 1.3,
irreducible_iteratedPoly).
Part of the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials,
Arch. Math. 59 (1992), 239-244; see QuadraticIterates.ArchMath1992.
Even factorizations and non-square c_n #
A reducible monic even polynomial with no nontrivial even divisors factors as
(-1) ^ (deg g) · p = g · g(-X): its irreducible factors pair up under X ↦ -X.
For irreducible F, every even divisor (d(-X) = d) of F ∘ (X² + c) is trivial — a unit
or associated to F ∘ (X² + c) — since it descends to a divisor of F.
Variant of isUnit_or_associated_of_dvd_comp for divisors that are even only up to
associates: if F is irreducible and the constant term of F ∘ (X² + c) is nonzero, then any
divisor d of F ∘ (X² + c) with d(-X) associated to d is a unit or associated to it.
Irreducibility of the iterates #
Lemma 1.2: if none of c_1, …, c_n is a square in ℚ, then f_n is irreducible over ℚ.
Corollary 1.3: all f_n (n ≥ 1) are irreducible over ℚ.
All f_n (including f_0 = X) are irreducible over ℚ when -a is not a square in ℚ;
this extends irreducible_iteratedPoly_of_pos to n = 0.
If -a = r ^ 2 in ℚ, then f_n = f_{n-1} ^ 2 + a = (f_{n-1} - r) * (f_{n-1} + r) factors
nontrivially, so irreducibility of any f_n with n ≥ 1 implies that -a is not a square.
This recovers the standing assumption of the paper from the irreducibility hypothesis of
Lemma 1.6.