The master expansion, integrality and the congruences

The end of the elementary route of §3 of Granville's paper. Expanding the numerator of the explicit form GranvilleMoore.iteratedFermatQuot_eq_sum_div along the Frobenius tower turns F^{(j)}_k(x) into a power series in p^{k+1} g_k(x) whose coefficients are the collapsed coefficients A_j(m) — the master expansion. Each of its terms is p-integral, so F^{(j)}_k(x) is an integer; and all but one of them is divisible by p, so reducing the expansion modulo p leaves the congruence j! F^{(j)}_k(x) ≡ x q_p(x)^j, with one extra surviving term in the single exceptional case j = p - 1, k = 0.

Main results

• GranvilleMoore.iteratedFermatQuot_eq_mul_sum: the master expansion F^{(j)}_k(x) = (x^{p^k}/p^{jk + C(j+1,2)}) ∑_{m ≤ e_j} A_j(m) (p^{k+1} g_k(x))^m.
• GranvilleMoore.pow_dvd_collapsedCoeff_mul_pow and GranvilleMoore.pow_succ_dvd_collapsedCoeff_mul_pow: the m-th term is p-integral, and divisible by p off the exceptional patterns.
• GranvilleMoore.exists_intCast_iteratedFermatQuot: F^{(j)}_k(x) ∈ ℤ for j ≤ p - 1.
• GranvilleMoore.dvd_factorial_mul_sub_mul_pow: j! F^{(j)}_k(x) ≡ x q_p(x)^j (mod p) for j ≤ p - 2.
• GranvilleMoore.dvd_factorial_mul_sub_exceptional: (p-1)! F^{(p-1)}_0(x) ≡ x q_p(x)^{p-1} - x q_p(x) (mod p).

Implementation notes

Everything is proved in ℤ. collapsedCoeff is ℚ-valued, but its defining sum has integer summands, so collapsedCoeff_eq_intCast exhibits it as the cast of an integer, and every statement that consumes a value of A_j(m), of g_k(x), of q_p(x) or of F^{(j)}_k(x) takes the representing integer as an argument together with the hypothesis identifying it — the house convention of GranvilleMoore.UnitQuotient. In particular numerator_eq_mul_sum, the integral core of the master expansion, is stated for an arbitrary A : ℕ → ℤ with ∀ m, collapsedCoeff p j m = (A m : ℚ); a consumer that only needs A opaquely obtains it from ⟨_, collapsedCoeff_eq_intCast p j⟩, and then no cast appears in the rest of its proof.

The integrality of a single term of the master expansion is usually stated as the valuation inequality v_p(A_j(m)) + m(k+1) - jk - C(j+1,2) ≥ 0, strict off m = j and (m, j, k) = (p, p-1, 0). That form is not usable: padicValRat p 0 = 0, so it says nothing at the pairs where A_j(m) vanishes — the same defect that forced the algebraic form of the valuation bound in GranvilleMoore.CollapsedCoeff. What is proved here instead is the divisibility p^{jk + C(j+1,2)} ∣ A_j(m) p^{m(k+1)}, respectively with one more factor of p, which is what the numerator of the m-th term being a multiple of the common denominator actually means, is unconditional, and is exactly what GranvilleMoore.exists_intCast_iteratedFermatQuot and the two congruences consume. All the p-adic bookkeeping is thereby concentrated in one place, pow_dvd_intCollapsedCoeff_mul_pow, whose only hypothesis is the arithmetic inequality D + v_p(m!) ≤ C(j,2) + m(k+1) on natural numbers; that inequality is where the case analysis on m < p, m = p, m > p lives, in padicValNat_factorial_add_le and padicValNat_factorial_add_lt, and it uses Legendre's bound in the sharp form (p-1) v_p(m!) < m.

The congruences are stated as divisibilities between integers rather than as congruences between rationals, again because the objects are ℚ-valued by definition. In both, the power p^{jk + C(j+1,2)} is cancelled by mul_left_cancel₀ after the surviving term has been identified, and the unit (p-1)^j — which enters because GranvilleMoore.CollapsedCoeff clears denominators by (p-1)^m rather than inverting them — is cancelled at the very end using that p ∤ p - 1.

For the exceptional congruence a weaker form allows an unspecified constant c ≡ 1 (mod p) on the x q_p(x) term. That constant is p A_{p-1}(p)/p^{C(p-1,2)} up to a factor of (p-1)! (p-1)^{p-1}, and dvd_sub_one_of_mul_eq computes it to be ≡ 1, so the clean form with coefficient exactly 1 is what is stated. The computation needs one coefficient of the rescaled binomial polynomial beyond the leading one, namely β_{p,p-1}; clearing denominators turns B_p into the monic ∏_{s<p}(X - (1 + s(p-1))), whose sub-leading coefficient is minus the sum of its roots, and that sum is divisible by p because twice it is p(2 + (p-1)^2).

The integer collapsed coefficient

Two elementary ingredients

The master expansion

theorem GranvilleMoore.iteratedFermatQuot_eq_mul_sum {p : ℕ} (hp : p ≠ 0) {x : ℤ} {j k : ℕ} {g : ℤ} (hg : unitQuot p x k = ↑g) : iteratedFermatQuot p j k x = ↑x ^ p ^ k / ↑p ^ (j * k + (j + 1).choose 2) * ∑ m ∈ Finset.range (frobeniusExponent p j + 1), collapsedCoeff p j m * (↑p ^ (k + 1) * ↑g) ^ m

lem_master_expansion: the master expansion of the iterated Fermat quotient,

F^{(j)}_k(x) = (x^{p^k} / p^{jk + C(j+1,2)}) * ∑_{m ≤ e_j} A_j(m) (p^{k+1} g_k(x))^m .

Writing y = x^{p^k} and u = y^{p-1} = t_x^{p^k}, the expansion u = 1 + p^{k+1} g_k(x) of GranvilleMoore.fermatUnit_pow_eq_one_add_pow_mul and the identity y^{p^i} = y u^{e_i} of GranvilleMoore.pow_pow_eq_mul_pow_frobeniusExponent turn each power x^{p^{k+i}} in the numerator of GranvilleMoore.iteratedFermatQuot_eq_sum_div into y times a Newton expansion in u - 1; exchanging the two finite sums leaves the coefficient ∑_{i ≤ j} (-1)^{j-i} c_{j,i} C(e_i,m), which is A_j(m), i.e. GranvilleMoore.collapsedCoeff p j m.

The sum is finite: C(e_i, m) = 0 once m > e_i, and e_i ≤ e_j for i ≤ j, so range (e_j + 1) already contains every nonvanishing index.

The valuation of the factorial

Each term of the master expansion is p-integral

theorem GranvilleMoore.pow_dvd_collapsedCoeff_mul_pow {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {j m k : ℕ} (hj : j ≤ p - 1) (hjm : j ≤ m) {A : ℤ} (hA : collapsedCoeff p j m = ↑A) : ↑p ^ (j * k + (j + 1).choose 2) ∣ A * ↑p ^ (m * (k + 1))

lem_master_term_integral, integrality: p^{jk + C(j+1,2)} divides A_j(m) p^{m(k+1)} for j ≤ p - 1 and m ≥ j, so the m-th term of the master expansion is p-integral.

The usual statement is the valuation inequality v_p(A_j(m)) + m(k+1) - jk - C(j+1,2) ≥ 0; this is its algebraic form, in which the numerator of the term is exhibited as a multiple of the denominator p^{jk + C(j+1,2)} of GranvilleMoore.iteratedFermatQuot_eq_sum_div. It reduces, via GranvilleMoore.exists_intCast_eq_factorial_mul_pow_mul_collapsedCoeff, to the arithmetic v_p(m!) + j(k+1) ≤ m(k+1) of padicValNat_factorial_add_le.

theorem GranvilleMoore.pow_succ_dvd_collapsedCoeff_mul_pow {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {j m k : ℕ} (hj : j ≤ p - 1) (hjm : j < m) (hexc : m ≠ p ∨ j ≠ p - 1 ∨ k ≠ 0) {A : ℤ} (hA : collapsedCoeff p j m = ↑A) : ↑p ^ (j * k + (j + 1).choose 2 + 1) ∣ A * ↑p ^ (m * (k + 1))

lem_master_term_integral, strict positivity: off the exceptional patterns m = j and (m, j, k) = (p, p - 1, 0) the divisibility of GranvilleMoore.pow_dvd_collapsedCoeff_mul_pow holds with one more factor of p, so the m-th term of the master expansion is divisible by p.

This is the second half of that lemma, and it is what makes only finitely many terms survive modulo p in GranvilleMoore.dvd_factorial_mul_sub_mul_pow and GranvilleMoore.dvd_factorial_mul_sub_exceptional.

Integrality

theorem GranvilleMoore.exists_intCast_iteratedFermatQuot {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {x : ℤ} (hx : ¬↑p ∣ x) {j : ℕ} (hj : j ≤ p - 1) (k : ℕ) : ∃ (z : ℤ), iteratedFermatQuot p j k x = ↑z

thm_fermat_integral: for an odd prime p with p ∤ x and 0 ≤ j ≤ p - 1, the iterated Fermat quotient F^{(j)}_k(x) is an integer, for every k.

Integrality is phrased as the existence of an integer whose cast is the value, matching GranvilleMoore.unitQuot_eq_intCast and GranvilleMoore.fermatQuotient_eq_intCast.

The proof stays in ℤ. The explicit form GranvilleMoore.iteratedFermatQuot_eq_sum_div exhibits F^{(j)}_k(x) as an integer numerator over p^{jk + C(j+1,2)}, so it is enough to divide the numerator by that power of p; the master expansion rewrites the numerator as a sum of terms each of which GranvilleMoore.pow_dvd_collapsedCoeff_mul_pow shows to be divisible by it.

The congruence

theorem GranvilleMoore.dvd_factorial_mul_sub_mul_pow {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {x : ℤ} (hx : ¬↑p ∣ x) {j : ℕ} (hj : j ≤ p - 2) (k : ℕ) {z q : ℤ} (hz : iteratedFermatQuot p j k x = ↑z) (hq : fermatQuotient p x = ↑q) : ↑p ∣ ↑j.factorial * z - x * q ^ j

thm_fermat_congruence: for an odd prime p with p ∤ x and 0 ≤ j ≤ p - 2,

j! F^{(j)}_k(x) ≡ x q_p(x)^j  (mod p) ,

stated as divisibility between the integers z representing F^{(j)}_k(x) (which exists by GranvilleMoore.exists_intCast_iteratedFermatQuot) and q representing q_p(x).

Only the term m = j of the master expansion survives modulo p: every other one is divisible by p by GranvilleMoore.pow_succ_dvd_collapsedCoeff_mul_pow, whose exceptional pattern needs j = p - 1 and is excluded by j ≤ p - 2. The surviving term is x^{p^k} (A_j(j)/p^{C(j,2)}) g_k(x)^j, and GranvilleMoore.exists_int_factorial_mul_pow_mul_collapsedCoeff_self supplies j! (p-1)^j A_j(j) = p^{C(j,2)} ((p-1)^j + p a). Reducing modulo p then uses x^{p^k} ≡ x (Fermat), g_k(x) ≡ q_p(x) (GranvilleMoore.dvd_unitQuot_sub_fermatQuotient) and finally cancels the unit (p-1)^j.

The exceptional congruence

theorem GranvilleMoore.dvd_factorial_mul_sub_exceptional {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {x : ℤ} (hx : ¬↑p ∣ x) {z q : ℤ} (hz : iteratedFermatQuot p (p - 1) 0 x = ↑z) (hq : fermatQuotient p x = ↑q) : ↑p ∣ ↑(p - 1).factorial * z - (x * q ^ (p - 1) - x * q)

thm_fermat_congruence_exceptional: for an odd prime p with p ∤ x,

(p-1)! F^{(p-1)}_0(x) ≡ x q_p(x)^{p-1} - x q_p(x)  (mod p) ,

stated as divisibility between the integers z representing F^{(p-1)}_0(x) and q representing q_p(x). A weaker form allows a constant c ≡ 1 (mod p) on the second term; that constant is here shown to be 1 on the nose, in agreement with the source paper.

This is the one pair (j, k) = (p-1, 0) at which GranvilleMoore.pow_succ_dvd_collapsedCoeff_mul_pow has an exception, so two terms of the master expansion survive modulo p: m = p - 1, contributing x q_p(x)^{p-1}/(p-1)! as in GranvilleMoore.dvd_factorial_mul_sub_mul_pow, and m = p, whose contribution is b x g_0(x)^p for the integer b with p A_{p-1}(p) = p^{C(p-1,2)} b. Since g_0(x)^p ≡ g_0(x) ≡ q_p(x) by Fermat and b ≡ 1 by dvd_sub_one_of_mul_eq, that second contribution is x q_p(x) times a unit; Wilson's theorem fixes the signs.