The main theorems

The integer factors b_n of the c-sequence — integral, pairwise coprime, and recovering c_n by Möbius inversion (Lemma 1.1 b) — and the three results of the paper: section1_equiv (Ω_n ≅ [C₂]ⁿ iff the c_i are 2-independent iff the b_i are), section1_squarefree (no |b_k| a square forces Ω_n ≅ [C₂]ⁿ) and section3_main (the congruence conditions on a that guarantee this for every n).

Part of the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; see QuadraticIterates.ArchMath1992.

The integer factors b_n

theorem QuadraticIterates.cSeq_ne_zero (a : ℤ) (ha : ¬IsSquare (-↑a)) {n : ℕ} (hn : 1 ≤ n) : cSeq a n ≠ 0

theorem QuadraticIterates.cSeq_factorization_shape (a : ℤ) (ha : ¬IsSquare (-↑a)) (q : ℤ) : Prime q → normalize q = q → ∃ m ≥ 1, ∃ (E : ℕ), ∀ k ≥ 1, (factorization (cSeq a k)) q = if m ∣ k then E else 0

The constant-valuation shape for c: the specialization of factorization_gammaSeq_shape to X² + a, ε = -1, in the form consumed by moebiusFactorR_isRelPrime.

theorem QuadraticIterates.intCast_bSeq (a : ℤ) (ha : ¬IsSquare (-↑a)) {n : ℕ} (hn : 1 ≤ n) : ↑(bSeq a n) = moebiusFactor (cSeq a) n

The image of b_n in ℚ is the Möbius product ∏_{ed = n} c_d^{μ(e)} (Lemma 1.1 b): the Möbius product of the c-sequence is the integer b_n, since c is a strong divisibility sequence.

theorem QuadraticIterates.bSeq_ne_zero (a : ℤ) (ha : ¬IsSquare (-↑a)) {n : ℕ} (hn : 1 ≤ n) : bSeq a n ≠ 0

theorem QuadraticIterates.cSeq_eq_prod_bSeq (a : ℤ) (ha : ¬IsSquare (-↑a)) {n : ℕ} (hn : 1 ≤ n) : cSeq a n = ∏ d ∈ n.divisors, bSeq a d

Möbius inversion for the integer factors (Lemma 1.1 b): c_n = ∏_{d ∣ n} b_d.

theorem QuadraticIterates.isCoprime_bSeq (a : ℤ) (ha : ¬IsSquare (-↑a)) {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hmn : m ≠ n) : IsCoprime (bSeq a m) (bSeq a n)

The integer factors b_n are pairwise coprime (Lemma 1.1 b): the valuation of b_n at each prime is supported on a single index, so no prime divides two distinct factors.

The main theorems

theorem QuadraticIterates.nonempty_mulEquiv_of_finrank_eq (a : ℤ) {n : ℕ} (hmax : Module.finrank ℚ ↥(splittingField a n) = 2 ^ (2 ^ n - 1)) : Nonempty (GaloisGroup a n ≃* WreathPower n)

theorem QuadraticIterates.section1_a_iff_b (a : ℤ) (ha : ¬IsSquare (-↑a)) (n : ℕ) : Nonempty (GaloisGroup a n ≃* WreathPower n) ↔ TwoIndependent fun (i : Fin n) => ↑(cSeq a (↑i + 1))

Section 1, (a) ↔ (b): Ω_n ≅ [C₂]ⁿ iff c_1, …, c_n are 2-independent.

theorem QuadraticIterates.sqClass_cSeq_eq_sum_divisors (a : ℤ) (ha : ¬IsSquare (-↑a)) {m : ℕ} (hm : 1 ≤ m) : sqClass ↑(cSeq a m) = ∑ d ∈ m.divisors, sqClass ↑(bSeq a d)

In ℚˣ/(ℚˣ)², the class of c_m is the sum of the classes of the b_d over d ∣ m.

theorem QuadraticIterates.sqClass_bSeq_eq_sum_divisorsAntidiagonal (a : ℤ) (ha : ¬IsSquare (-↑a)) {m : ℕ} (hm : 1 ≤ m) : sqClass ↑(bSeq a m) = ∑ x ∈ m.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • sqClass ↑(cSeq a x.2)

In ℚˣ/(ℚˣ)², the class of b_m is the Möbius-weighted sum of the classes of the c_d.

theorem QuadraticIterates.section1_b_iff_c (a : ℤ) (ha : ¬IsSquare (-↑a)) (n : ℕ) : (TwoIndependent fun (i : Fin n) => ↑(cSeq a (↑i + 1))) ↔ TwoIndependent fun (i : Fin n) => ↑(bSeq a (↑i + 1))

Section 1, (b) ↔ (c): c_1, …, c_n are 2-independent iff b_1, …, b_n are 2-independent.

theorem QuadraticIterates.section1_equiv (a : ℤ) (ha : ¬IsSquare (-↑a)) (n : ℕ) : [Nonempty (GaloisGroup a n ≃* WreathPower n), TwoIndependent fun (i : Fin n) => ↑(cSeq a (↑i + 1)), TwoIndependent fun (i : Fin n) => ↑(bSeq a (↑i + 1))].TFAE

Theorem (Section 1), part 1: Ω_n ≅ [C_2]^n iff c_1, …, c_n are 2-independent iff b_1, …, b_n are 2-independent.

theorem QuadraticIterates.section1_squarefree (a : ℤ) (ha : ¬IsSquare (-↑a)) (n : ℕ) (h : ∀ k ≥ 2, k ≤ n → ¬IsSquare |bSeq a k|) : Nonempty (GaloisGroup a n ≃* WreathPower n)

Theorem (Section 1), part 2: if none of |b_2|, …, |b_n| is a square in ℚ, then Ω_n ≅ [C_2]^n.

theorem QuadraticIterates.abs_cSeq_eq_gammaSeq_mul_abs (a : ℤ) (ha : ¬IsSquare (-↑a)) (d : ℕ) : d ≥ 1 → |cSeq a d| = gammaSeq (normPoly a) a.sign d * |a|

theorem QuadraticIterates.gammaSeq_normPoly_pos (a : ℤ) (ha : ¬IsSquare (-↑a)) (d : ℕ) : d ≥ 1 → 0 < gammaSeq (normPoly a) a.sign d

theorem QuadraticIterates.abs_bSeq_eq_betaSeq (a : ℤ) (ha : ¬IsSquare (-↑a)) (n : ℕ) : n ≥ 2 → |bSeq a n| = betaSeq (normPoly a) a.sign n

theorem QuadraticIterates.section3_main (a : ℤ) (hcase : 0 < a ∧ a % 4 = 1 ∨ 0 < a ∧ a % 4 = 2 ∨ a < 0 ∧ a % 4 = 0 ∧ ¬IsSquare (-a)) (n : ℕ) : n ≥ 1 → Nonempty (GaloisGroup a n ≃* WreathPower n)

Section 3, main result: if a > 0 and a ≡ 1 or 2 mod 4, or a < 0, a ≡ 0 mod 4 and -a is not a square, then Gal(f_n/ℚ) ≅ [C_2]^n for all n ≥ 1.