The coefficient analysis

The combinatorial core of the elementary route to the congruences for the iterated Fermat quotients. Nothing here mentions the Moore determinant: these are facts about the coefficients of cPoly and about products of differences of powers of p.

Main results

• GranvilleMoore.cCoeff_succ: the recursion c_{j+1,i+1} = c_{j,i} + p^j c_{j,i+1}.
• GranvilleMoore.signedCCoeff_sum_eq_prod: the signed coefficient identity ∑_{i ≤ j} (-1)^{j-i} c_{j,i} z^i = ∏_{r<j} (z - p^r).
• GranvilleMoore.prod_pow_sub_pow_eq_zero: that product vanishes when n < j.
• GranvilleMoore.prod_pow_sub_pow_eq_pow_mul: for j ≤ n it factors as p^{∑_{r<j} r} times a product of units.
• GranvilleMoore.sum_range_choose_two: the hockey stick ∑_{c ≤ d} C(c,2) = C(d+1,3).

Implementation notes

The signed identity is stated evaluated at an integer z rather than as an identity of polynomials. That is the only form the consumer needs — the collapsed coefficient is ∑_i (-1)^{j-i} c_{j,i} (e_i choose m) and the analysis evaluates it at z = p^n — and it avoids composing cPoly with -X to get there.

prod_pow_sub_pow_eq_pow_mul leaves the exponent as ∑ r ∈ range j, r rather than C(j,2); keeping the sum makes the proof one Finset.prod_congr. To convert, use Finset.sum_range_id together with Nat.choose_two_right — there is no single Mathlib lemma for it, and in particular no Finset.sum_range_id_eq_choose_two, which does not exist.

The recursion for the coefficients

theorem GranvilleMoore.cCoeff_succ (p j i : ℕ) : cCoeff p (j + 1) (i + 1) = cCoeff p j i + ↑p ^ j * cCoeff p j (i + 1)

Recursion for the coefficients: c_{j+1,i+1} = c_{j,i} + p^j c_{j,i+1}.

Stated at i + 1 so that the paper's c_{j,i-1} is subtraction-free.

The signed coefficient identity

theorem GranvilleMoore.signedCCoeff_sum_eq_prod (p j : ℕ) (z : ℤ) : ∑ i ∈ Finset.range (j + 1), (-1) ^ (j - i) * cCoeff p j i * z ^ i = ∏ r ∈ Finset.range j, (z - ↑p ^ r)

The signed coefficient identity, evaluated: ∑_{i ≤ j} (-1)^{j-i} c_{j,i}(p) z^i = ∏_{r<j} (z - p^r).

Substituting -z into the defining product of cPoly and pulling out (-1)^j. Evaluated at z = p^n this is what turns the collapsed coefficient into a product of differences of powers of p.

Products of differences of powers of p

theorem GranvilleMoore.prod_pow_sub_pow_eq_zero {p n j : ℕ} (h : n < j) : ∏ r ∈ Finset.range j, (↑p ^ n - ↑p ^ r) = 0

The p-power difference product vanishes for n < j: the factor at r = n is p^n - p^n = 0.

theorem GranvilleMoore.prod_pow_sub_pow_eq_pow_mul {p n j : ℕ} (h : j ≤ n) : ∏ r ∈ Finset.range j, (↑p ^ n - ↑p ^ r) = (↑p ^ ∑ r ∈ Finset.range j, r) * ∏ r ∈ Finset.range j, (↑p ^ (n - r) - 1)

For j ≤ n the product factors as p^{∑_{r<j} r} times a product of terms p^{n-r} - 1, each of which is ≡ -1 mod p and so a unit.

This is the paper's ∏_{r<j}(p^{m-r} - 1) with its power of p made explicit; the exponent ∑ r ∈ range j, r equals C(j,2) by Finset.sum_range_id and Nat.choose_two_right.

The ladder exponent

theorem GranvilleMoore.sum_range_choose_two (d : ℕ) : ∑ c ∈ Finset.range (d + 1), c.choose 2 = (d + 1).choose 3

The ladder exponent: ∑_{c ≤ d} C(c,2) = C(d+1,3), the hockey stick.

The i-th rung of the reduction ladder contributes C(d-i,2); re-indexing by c = d - i turns the ladder's total into this sum, which is how GranvilleMoore.sum_range_sub_choose_two — that total in the ladder's own indexing — is proved.