Exact p-adic valuations of differences of powers

This file complements Mathlib's lifting-the-exponent lemmas in Mathlib/NumberTheory/Multiplicity.lean. The valuation of n at p is Mathlib's multiplicity p n on ℕ.

Exact valuations of a ^ k - b ^ k

Let p be a prime not dividing a * b and let d be the order of a / b modulo p, so that p ∣ a ^ k - b ^ k exactly when d ∣ k. The first group of results computes the exact power of p dividing a ^ k - b ^ k for every positive multiple k of d, in terms of a ^ d - b ^ d and k.

• For an odd prime p with p ∤ d and b < a, v_p(a ^ k - b ^ k) = v_p(a ^ d - b ^ d) + v_p(k).
• For p = 2 the bases are odd and d = 1: v₂(a ^ k - b ^ k) = v₂(a - b) for odd k, and v₂(a ^ k - b ^ k) + 1 = v₂(a ^ 2 - b ^ 2) + v₂(k) for b < a and even k ≠ 0.

The order d enters only through p ∣ a ^ d - b ^ d and p ∤ d, so the statements are phrased with an arbitrary d subject to these hypotheses. They are the lifting-the-exponent input for the valuation of two-variable cyclotomic values and for the nonprimitive prime divisors of a ^ n - b ^ n in the Bang–Zsigmondy theorem. All of them reduce to Mathlib's emultiplicity_pow_sub_pow_of_prime, Nat.multiplicity_pow_sub_pow and Nat.multiplicity_pow_two_sub_pow.

Lifting a residue so that b ^ n - 1 has exact p-adic valuation

Let p be a prime and n a natural number prime to p. If b₀ ^ n ≡ 1 (mod p ^ k), then b₀ can be moved within its residue class modulo p ^ k so that p ^ k divides b ^ n - 1 exactly, that is, so that b ^ n - 1 has p-adic valuation exactly k.

In the computation of the generator rank of the absolute Galois group of a p-adic field (NSW (7.4.1)), this chooses the exponent through which a generator of tame inertia acts on the p-power roots of unity.

Main statements

• Nat.multiplicity_pow_sub_pow_of_not_dvd: for any prime p with p ∣ x - y, p ∤ x and p ∤ n, the valuations of x ^ n - y ^ n and x - y at p agree.
• Nat.multiplicity_pow_sub_pow_of_dvd_pow_sub_pow: for an odd prime p and y < x with p ∣ x ^ d - y ^ d, p ∤ x, p ∤ d and d ∣ n ≠ 0, v_p(x ^ n - y ^ n) = v_p(x ^ d - y ^ d) + v_p(n).
• Nat.multiplicity_pow_two_sub_pow_of_odd: for odd x, y and odd n, v₂(x ^ n - y ^ n) = v₂(x - y).
• Nat.multiplicity_pow_two_sub_pow_of_even: for odd y < x and even n ≠ 0, v₂(x ^ n - y ^ n) + 1 = v₂(x ^ 2 - y ^ 2) + v₂(n).
• TauCeti.exists_modEq_pow_sub_one_eq_mul: the lift with b ^ n - 1 = p ^ k * c, p ∤ c.

References

• G. D. Birkhoff and H. S. Vandiver, On the integral divisors of a ^ n - b ^ n, Ann. of Math. (2) 5 (1904), 173–180, Theorem III, p. 175.
• Ö. Avcı, Large Zsigmondy primes, arXiv:2011.06136v2 (2023), Lemma 2.2.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, proof of (7.4.1).

theorem Nat.multiplicity_pow_sub_pow_of_not_dvd {p : ℕ} [hp : Fact (Prime p)] {x y n : ℕ} (hxy : p ∣ x - y) (hx : ¬p ∣ x) (hn : ¬p ∣ n) : multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y)

For any prime p, including p = 2, with p ∣ x - y and p ∤ x, raising to an exponent n prime to p does not change the valuation at p: v_p(x ^ n - y ^ n) = v_p(x - y). No ordering of x and y is needed, since both sides vanish when x ≤ y.

theorem Nat.multiplicity_pow_sub_pow_of_dvd_pow_sub_pow {p : ℕ} [hp : Fact (Prime p)] (hp1 : Odd p) {x y d n : ℕ} (hyx : y < x) (hxy : p ∣ x ^ d - y ^ d) (hx : ¬p ∣ x) (hd : ¬p ∣ d) (hdn : d ∣ n) (hn : n ≠ 0) : multiplicity p (x ^ n - y ^ n) = multiplicity p (x ^ d - y ^ d) + multiplicity p n

Lifting the exponent from an intermediate exponent d: for an odd prime p and y < x with p ∣ x ^ d - y ^ d, p ∤ x and p ∤ d, every nonzero multiple n of d satisfies v_p(x ^ n - y ^ n) = v_p(x ^ d - y ^ d) + v_p(n). Taking for d the order of x / y modulo p gives the valuation of x ^ n - y ^ n at every exponent n it divides.

theorem Nat.multiplicity_pow_two_sub_pow_of_odd {x y n : ℕ} (hx : Odd x) (hy : Odd y) (hn : Odd n) : multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y)

For odd x and y and an odd exponent n, v₂(x ^ n - y ^ n) = v₂(x - y).

theorem Nat.multiplicity_pow_two_sub_pow_of_even {x y n : ℕ} (hyx : y < x) (hx : Odd x) (hy : Odd y) (hn : Even n) (hn0 : n ≠ 0) : multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x ^ 2 - y ^ 2) + multiplicity 2 n

Lifting the exponent at p = 2 for an even exponent: for odd y < x and even n ≠ 0, v₂(x ^ n - y ^ n) + 1 = v₂(x ^ 2 - y ^ 2) + v₂(n). The odd-prime formula of Nat.multiplicity_pow_sub_pow_of_dvd_pow_sub_pow fails here: at (x, y, n) = (3, 1, 2) it would give v₂(8) = v₂(2) + v₂(2) = 2, not 3.

theorem TauCeti.exists_modEq_pow_sub_one_eq_mul {p : ℕ} [Fact (Nat.Prime p)] {k n b₀ : ℕ} (hn : ¬p ∣ n) (hb₀ : b₀ ^ n ≡ 1 [MOD p ^ k]) : ∃ (b : ℕ), b ≡ b₀ [MOD p ^ k] ∧ ∃ (c : ℤ), ↑b ^ n - 1 = ↑p ^ k * c ∧ ¬↑p ∣ c

A lift b₀ of a unit of order dividing n modulo p ^ k, with p ∤ n, can be moved by a multiple of p ^ k so that b ^ n - 1 has p-adic valuation exactly k.