The iteration sequence of a polynomial and its Möbius factors

For g ∈ R[X] and a sign ε, the sequence γ_1 = ε · g(0), γ_{n+1} = g(γ_n) and its Möbius factors β_n = ∏_{d ∣ n} γ_d^{μ(n/d)}. The results are stated at the generality each one needs: over a CommSemiring for the recursion, over a CommRing for the congruences, over a GCD domain for strong divisibility (gammaSeq_associated_gcd), over a UFD for the valuation shape (factorization_gammaSeq_shape) and the integrality of β, and finally over ℤ for Lemmas 2.1 and 2.2 of the paper (not_isSquare_betaSeq and not_isSquare_betaSeq_of_pos).

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

The sequences γ and β, and even polynomials

def QuadraticIterates.gammaSeq {R : Type u_1} [CommSemiring R] (g : Polynomial R) (ε : R) : ℕ → R

The iteration sequence γ_n of g ∈ R[X] with sign choice ε: γ_1 = ε · g(0), γ_{n+1} = g(γ_n); the value at index 0 is 0 (chosen so that over ℤ, γ is a strong divisibility sequence).

Equations

• QuadraticIterates.gammaSeq g ε 0 = 0
• QuadraticIterates.gammaSeq g ε 1 = ε * Polynomial.eval 0 g
• QuadraticIterates.gammaSeq g ε n.succ.succ = Polynomial.eval (QuadraticIterates.gammaSeq g ε (n + 1)) g

noncomputable def QuadraticIterates.betaSeq {R : Type u_1} [CommRing R] [IsDomain R] (g : Polynomial R) (ε : R) (n : ℕ) : R

The Möbius factors β_n = ∏_{d ∣ n} γ_d^{μ(n/d)} of the γ-sequence, as elements of the coefficient ring: the unique preimage of the fraction-field Möbius product under R → FractionRing R (junk when that product is not integral).

Equations

• QuadraticIterates.betaSeq g ε n = moebiusFactorR (QuadraticIterates.gammaSeq g ε) n

theorem QuadraticIterates.betaSeq_eq_moebiusFactorR {R : Type u_1} [CommRing R] [IsDomain R] (g : Polynomial R) (ε : R) (n : ℕ) : betaSeq g ε n = moebiusFactorR (gammaSeq g ε) n

def QuadraticIterates.EvenPoly {R : Type u_1} [CommSemiring R] (g : Polynomial R) : Prop

g is an even polynomial (g ∈ R[X²]): g = Polynomial.expand R 2 h for some h.

Equations

• QuadraticIterates.EvenPoly g = ∃ (h : Polynomial R), g = (Polynomial.expand R 2) h

theorem QuadraticIterates.EvenPoly.eval_congr {R : Type u_1} [CommSemiring R] {g : Polynomial R} (hg : EvenPoly g) {x y : R} (h : x ^ 2 = y ^ 2) : Polynomial.eval x g = Polynomial.eval y g

An even polynomial takes equal values at points with equal squares.

theorem QuadraticIterates.EvenPoly.eval_neg {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) (y : R) : Polynomial.eval (-y) g = Polynomial.eval y g

An even polynomial defines an even evaluation function.

theorem QuadraticIterates.EvenPoly.map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {g : Polynomial R} (hg : EvenPoly g) (φ : R →+* S) : EvenPoly (Polynomial.map φ g)

Being an even polynomial is preserved by ring homomorphisms.

theorem QuadraticIterates.EvenPoly.dvd_eval_sub {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) {N a b : R} (h : N ∣ a ^ 2 - b ^ 2) : N ∣ Polynomial.eval a g - Polynomial.eval b g

theorem QuadraticIterates.EvenPoly.comp_neg_X {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) : g.comp (-Polynomial.X) = g

An even polynomial is fixed by X ↦ -X.

theorem QuadraticIterates.evenPoly_iff_comp_neg_X {R : Type u_1} [CommRing R] [NoZeroDivisors R] [NeZero 2] {g : Polynomial R} : EvenPoly g ↔ g.comp (-Polynomial.X) = g

Over a domain of characteristic ≠ 2 the converse holds too, so the two notions of evenness this file uses — membership in R[X²] and invariance under X ↦ -X — agree.

The γ-sequence over a commutative semiring

@[simp]

theorem QuadraticIterates.gammaSeq_zero {R : Type u_1} [CommSemiring R] (g : Polynomial R) (ε : R) : gammaSeq g ε 0 = 0

@[simp]

theorem QuadraticIterates.gammaSeq_one {R : Type u_1} [CommSemiring R] (g : Polynomial R) (ε : R) : gammaSeq g ε 1 = ε * Polynomial.eval 0 g

theorem QuadraticIterates.gammaSeq_succ {R : Type u_1} [CommSemiring R] (g : Polynomial R) (ε : R) {n : ℕ} (hn : 1 ≤ n) : gammaSeq g ε (n + 1) = Polynomial.eval (gammaSeq g ε n) g

The recursion γ_{n+1} = g(γ_n), valid for n ≥ 1.

theorem QuadraticIterates.gammaSeq_add {R : Type u_1} [CommSemiring R] (g : Polynomial R) (ε : R) {m : ℕ} (hm : 1 ≤ m) (n : ℕ) : gammaSeq g ε (m + n) = (fun (z : R) => Polynomial.eval z g)^[n] (gammaSeq g ε m)

theorem QuadraticIterates.map_gammaSeq {R : Type u_1} [CommSemiring R] (g : Polynomial R) {S : Type u_2} [CommSemiring S] (φ : R →+* S) (ε : R) (n : ℕ) : φ (gammaSeq g ε n) = gammaSeq (Polynomial.map φ g) (φ ε) n

A ring homomorphism intertwines the γ-sequences of g and its image: φ(γ_n(g, ε)) = γ_n(g.map φ, φ ε).

theorem QuadraticIterates.gammaSeq_one_succ {R : Type u_1} [CommSemiring R] (g : Polynomial R) (n : ℕ) : gammaSeq g 1 (n + 1) = Polynomial.eval (gammaSeq g 1 n) g

The recursion γ_{n+1} = g(γ_n) for the ε = 1 sequence, valid at every index (including 0, since γ_0 = 0 and γ_1 = g(0)).

theorem QuadraticIterates.gammaSeq_add_succ_eq_three {R : Type u_1} [CommSemiring R] {g : Polynomial R} (hg : EvenPoly g) (h4 : 4 = 0) (h0 : Polynomial.eval 0 g = 1) (h1 : Polynomial.eval 1 g = 2) (n : ℕ) : n ≥ 1 → gammaSeq g 1 n + gammaSeq g 1 (n + 1) = 3

In a ring with 4 = 0, the ε = 1 sequence of an even g with g(0) = 1, g(1) = 2 alternates between 1 and 2, so consecutive terms sum to 3. (The only property of ZMod 4 used in the mod-4 step is 4 = 0, which gives g(2) = g(0) by evenness.)

theorem QuadraticIterates.gammaSeq_add_succ_eq_two_mul_eval_one {R : Type u_1} [CommSemiring R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} (hε : ε ^ 2 = 1) (h0 : Polynomial.eval 0 g ^ 2 = 1) (h1 : Polynomial.eval 1 g ^ 2 = 1) (n : ℕ) : n ≥ 2 → gammaSeq g ε n + gammaSeq g ε (n + 1) = 2 * Polynomial.eval 1 g

If ε² = g(0)² = g(1)² = 1 and g is even, then γ_n = g(1) for all n ≥ 2, so consecutive terms sum to 2·g(1). (The only property of ZMod 8 used in the mod-8 step is that the relevant residues square to 1.)

theorem QuadraticIterates.gammaSeq_eq_gammaSeq_one {R : Type u_1} [CommSemiring R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} (hε : ε ^ 2 = 1) {n : ℕ} (hn : 2 ≤ n) : gammaSeq g ε n = gammaSeq g 1 n

For even g and ε² = 1, the ε-sequence equals the ε = 1 sequence from index 2 on: the sign is absorbed by the square inside g.

theorem QuadraticIterates.gammaSeq_associated_one {R : Type u_1} [CommSemiring R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} (hε : ε ^ 2 = 1) (n : ℕ) : Associated (gammaSeq g ε n) (gammaSeq g 1 n)

For even g and ε² = 1, the ε-sequence is associated to the ε = 1 sequence: the two agree from index 2 on and differ by the unit ε at index 1.

The γ-sequence over a commutative ring

theorem QuadraticIterates.gammaSeq_associated_gcd {R : Type u_1} [CommRing R] {g : Polynomial R} [IsDomain R] [NormalizedGCDMonoid R] (hg : EvenPoly g) {ε : R} (hε : ε ^ 2 = 1) (m n : ℕ) : Associated (gcd (gammaSeq g ε m) (gammaSeq g ε n)) (gammaSeq g ε (m.gcd n))

Strong divisibility of the γ-sequence over a GCD domain: for even g and ε² = 1, gcd (γ_m) (γ_n) is associated to γ_{gcd m n}.

theorem QuadraticIterates.gammaSeq_period {R : Type u_1} [CommRing R] (g : Polynomial R) {ε : R} {m n₀ : ℕ} (hn₀ : 1 ≤ n₀) {q : R} (hbase : q ∣ gammaSeq g ε (n₀ + m) - gammaSeq g ε n₀) (n : ℕ) : n ≥ n₀ → q ∣ gammaSeq g ε (n + m) - gammaSeq g ε n

Periodicity propagates along the recursion: a divisor of γ_{n₀+m} - γ_{n₀} divides γ_{n+m} - γ_n for all n ≥ n₀ ≥ 1.

theorem QuadraticIterates.sq_dvd_gammaSeq_succ_sub {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) (ε : R) {n : ℕ} (hn : 1 ≤ n) : gammaSeq g ε n ^ 2 ∣ gammaSeq g ε (n + 1) - Polynomial.eval 0 g

For even g, γ_n ^ 2 divides γ_{n+1} - g(0) (n ≥ 1).

theorem QuadraticIterates.pow_succ_dvd_gammaSeq_succ_sub {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} {n : ℕ} (hn : 1 ≤ n) {p : R} {E : ℕ} (hE : 1 ≤ E) (hpE : p ^ E ∣ gammaSeq g ε n) : p ^ (E + 1) ∣ gammaSeq g ε (n + 1) - Polynomial.eval 0 g

Sharpening of sq_dvd_gammaSeq_succ_sub: a prime power p^E with E ≥ 1 dividing γ_n already forces p^{E+1} ∣ γ_{n+1} - g(0) (n ≥ 1).

theorem QuadraticIterates.gammaSeq_mul_eq_two_mul {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} {k : ℕ} (hk : 1 ≤ k) (hzero : gammaSeq g ε k + gammaSeq g ε (2 * k) = 0) (l : ℕ) : l ≥ 2 → gammaSeq g ε (l * k) = gammaSeq g ε (2 * k)

If γ_k + γ_{2k} = 0, then γ_{lk} = γ_{2k} for all l ≥ 2 (over any ring, for even g): γ is constant on positive multiples of k past the first.

theorem QuadraticIterates.prod_gammaSeq_mul_eq {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} {k : ℕ} (hk : 1 ≤ k) (hzero : gammaSeq g ε k + gammaSeq g ε (2 * k) = 0) {S : Finset ℕ} (hS : ∀ t ∈ S, 1 ≤ t) : ∏ t ∈ S, gammaSeq g ε (k * t) = gammaSeq g ε (2 * k) ^ S.card * if 1 ∈ S then -1 else 1

If γ_k + γ_{2k} = 0, then a product ∏_{t ∈ S} γ_{kt} over positive indices t collapses to γ_{2k} ^ |S| up to a sign recording whether 1 ∈ S (over any ring, for even g).

theorem QuadraticIterates.gammaSeq_add_eq_succ {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} {n : ℕ} (hn : 1 ≤ n) (hzero : gammaSeq g ε n + gammaSeq g ε (n + 1) = 0) (j : ℕ) : j ≥ 1 → gammaSeq g ε (n + j) = gammaSeq g ε (n + 1)

If γ_n + γ_{n+1} = 0, then γ_{n+j} = γ_{n+1} for all j ≥ 1 (over any ring, for even g): the fixed-point relation g(γ_{n+1}) = γ_{n+1} makes γ constant past index n.

theorem QuadraticIterates.gammaSeq_add_succ_dvd {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : EvenPoly g) (ε : R) {n : ℕ} (hn : 1 ≤ n) : gammaSeq g ε n + gammaSeq g ε (n + 1) ∣ gammaSeq g ε n + gammaSeq g ε (2 * n)

For even g, γ_n + γ_{n+1} divides γ_n + γ_{2n} (n ≥ 1): modulo the left-hand side the sequence is constant from index n + 1 on, so γ_{2n} ≡ γ_{n+1}.

theorem QuadraticIterates.isCoprime_gammaSeq_add_succ {R : Type u_1} [CommRing R] (g : Polynomial R) (ε : R) {n : ℕ} (hn : 1 ≤ n) (h0 : IsUnit (Polynomial.eval 0 g)) : IsCoprime (gammaSeq g ε n + gammaSeq g ε (n + 1)) (gammaSeq g ε n)

γ_{n+1} ≡ g(0) modulo γ_n, so γ_n + γ_{n+1} and γ_n are coprime once g(0) is a unit (n ≥ 1).

Valuations of the γ-sequence over a UFD

theorem QuadraticIterates.factorization_gammaSeq_of_dvd_eval_zero {R : Type u_1} [CommRing R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} (hε : ε ^ 2 = 1) (hne : ∀ k ≥ 1, gammaSeq g ε k ≠ 0) {p : R} (hp : Prime p) (hpn : normalize p = p) (hpg : p ∣ Polynomial.eval 0 g) {n : ℕ} (hn : 1 ≤ n) : (factorization (gammaSeq g ε n)) p = (factorization (Polynomial.eval 0 g)) p

If p ∣ g(0), the valuation v_p(γ_n) is the constant v_p(g(0)).

theorem QuadraticIterates.factorization_gammaSeq_shape {R : Type u_1} [CommRing R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {g : Polynomial R} (hg : EvenPoly g) {ε : R} (hε : ε ^ 2 = 1) (hne : ∀ k ≥ 1, gammaSeq g ε k ≠ 0) {p : R} (hp : Prime p) (hpn : normalize p = p) : ∃ m ≥ 1, ∃ (E : ℕ), ∀ n ≥ 1, (factorization (gammaSeq g ε n)) p = if m ∣ n then E else 0

Constant-valuation shape of the γ-sequence over a UFD (for even g, ε² = 1, γ nowhere zero): for each normalized prime p, the valuation v_p(γ_n) equals a constant E on the multiples of some index m ≥ 1 and vanishes elsewhere.

The γ- and β-sequences over ℤ

noncomputable def QuadraticIterates.moebiusFactor (c : ℕ → ℤ) (n : ℕ) : ℚ

The Möbius factor ∏_{d ∣ n} c_d^{μ(n/d)} of an integer sequence c, as a product over the divisor antidiagonal of n: pairs (e, d) with e * d = n contribute c_d ^ μ(e). Rational, as μ can be negative; it is an integer when c is a strong divisibility sequence.

Equations

• QuadraticIterates.moebiusFactor c n = ∏ x ∈ n.divisorsAntidiagonal, ↑(c x.2) ^ ArithmeticFunction.moebius x.1

theorem QuadraticIterates.moebiusFactor_eq_prod (c : ℕ → ℤ) (n : ℕ) : moebiusFactor c n = ∏ x ∈ n.divisorsAntidiagonal, ↑(c x.2) ^ ArithmeticFunction.moebius x.1

theorem QuadraticIterates.associated_gcd_of_int_gcd_eq_natAbs {c : ℕ → ℤ} (hsd : ∀ (m n : ℕ), (c m).gcd (c n) = (c (m.gcd n)).natAbs) (m n : ℕ) : Associated (gcd (c m) (c n)) (c (m.gcd n))

Strong divisibility over ℤ, translated from the Int.gcd/natAbs form into the Associated-of-GCDMonoid.gcd form consumed by the moebiusFactorR API.

theorem QuadraticIterates.intCast_moebiusFactorR {c : ℕ → ℤ} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), (c m).gcd (c n) = (c (m.gcd n)).natAbs) {n : ℕ} (hn : 1 ≤ n) : ↑(moebiusFactorR c n) = moebiusFactor c n

Over ℤ, the image in ℚ of the integer-valued Möbius factor moebiusFactorR is the ℚ-valued Möbius product moebiusFactor, for a strong divisibility sequence.

theorem QuadraticIterates.intCast_gammaSeq (g : Polynomial ℤ) (ε : ℤ) (S : Type u_1) [CommRing S] (i : ℕ) : ↑(gammaSeq g ε i) = gammaSeq (Polynomial.map (Int.castRingHom S) g) (↑ε) i

The image in a ring S of the ε-sequence over ℤ is the ε-sequence of the image of g: (γ_n : S) = γ_n(g.map (· : ℤ → S), ε).

theorem QuadraticIterates.gammaSeq_gcd {g : Polynomial ℤ} (hg : EvenPoly g) {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (m n : ℕ) : (gammaSeq g ε m).gcd (gammaSeq g ε n) = (gammaSeq g ε (m.gcd n)).natAbs

Strong divisibility over ℤ, for even g and ε = ±1: gcd (γ_m) (γ_n) = |γ_{gcd m n}|.

theorem QuadraticIterates.intCast_betaSeq {g : Polynomial ℤ} (hg : EvenPoly g) {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (hγ : ∀ k ≥ 1, gammaSeq g ε k ≠ 0) (n : ℕ) (hn : 1 ≤ n) : ↑(betaSeq g ε n) = moebiusFactor (gammaSeq g ε) n

The image of β_n in ℚ is the Möbius product ∏_{ed = n} γ_d^{μ(e)} (for even g, ε = ±1, and γ nowhere zero on positive indices).

theorem QuadraticIterates.not_isSquare_betaSeq {g : Polynomial ℤ} (hg : EvenPoly g) {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (hγ : ∀ n ≥ 1, gammaSeq g ε n ≠ 0) (hm : ∀ n ≥ 1, ∃ (m : ℕ), ↑m ∣ gammaSeq g ε n + gammaSeq g ε (2 * n) ∧ IsCoprime (↑m) (gammaSeq g ε n) ∧ ¬IsSquare (-1)) (n : ℕ) : n ≥ 2 → ¬IsSquare ↑(betaSeq g ε n)

Lemma 2.1: if for each n ≥ 1 some m divides γ_n + γ_{2n}, is prime to γ_n, and -1 is not a square mod m, then β_n is not a square in ℚ for n ≥ 2.

theorem QuadraticIterates.gammaSeq_add_succ_zmod_four_eq_three {g : Polynomial ℤ} (hg : EvenPoly g) (h0 : Polynomial.eval 0 g = 1) (h1 : ↑(Polynomial.eval 1 g) = 2) (n : ℕ) : n ≥ 1 → ↑(gammaSeq g 1 n + gammaSeq g 1 (n + 1)) = 3

The ZMod 4 specialization of gammaSeq_add_succ_eq_three via intCast_gammaSeq.

theorem QuadraticIterates.gammaSeq_add_succ_zmod_eight_eq_six {g : Polynomial ℤ} (hg : EvenPoly g) {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (h0 : Polynomial.eval 0 g = 1 ∨ Polynomial.eval 0 g = -1) (h1 : ↑(Polynomial.eval 1 g) = 3) (n : ℕ) : n ≥ 2 → ↑(gammaSeq g ε n + gammaSeq g ε (n + 1)) = 6

The ZMod 8 specialization of gammaSeq_add_succ_eq_two_mul_eval_one via intCast_gammaSeq; the mod-4 hypothesis on g(1) transfers through the canonical map ZMod 8 → ZMod 4.

theorem QuadraticIterates.not_isSquare_betaSeq_of_pos {g : Polynomial ℤ} (hg : EvenPoly g) {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (hpos : ∀ n ≥ 1, 0 < gammaSeq g ε n) (hcase : Polynomial.eval 0 g = 1 ∧ Polynomial.eval 1 g % 4 = 2 ∨ (Polynomial.eval 0 g = 1 ∨ Polynomial.eval 0 g = -1) ∧ Polynomial.eval 1 g % 4 = 3) (n : ℕ) : n ≥ 2 → ¬IsSquare ↑(betaSeq g ε n)

Lemma 2.2: if all γ_n > 0 and either g(0) = 1, g(1) ≡ 2 mod 4, or g(0) = ±1, g(1) ≡ 3 mod 4, then β_n is not a square in ℚ for n ≥ 2.