The collapsed coefficient

The four facts about A_j(m) that the master expansion needs. The definition GranvilleMoore.collapsedCoeff is a sum over i ≤ j of signed c-coefficients against binomial coefficients C(e_i, m); expanding each C(e_i, m) as a polynomial in p^i and exchanging the two sums replaces it by a sum over n ≤ m of β_{m,n} against a product of differences of powers of p. Everything else here is read off that closed form.

Main results

• GranvilleMoore.collapsedCoeff_eq_sum: A_j(m) = ∑_{n ≤ m} β_{m,n} ∏_{r<j}(p^n - p^r).
• GranvilleMoore.collapsedCoeff_eq_zero: A_j(m) = 0 for m < j.
• GranvilleMoore.exists_intCast_eq_factorial_mul_pow_mul_collapsedCoeff and GranvilleMoore.le_padicValRat_collapsedCoeff: m! (p-1)^m A_j(m) / p^{C(j,2)} is an integer, and hence v_p(A_j(m)) ≥ C(j,2) - v_p(m!).
• GranvilleMoore.collapsedCoeff_self_eq, GranvilleMoore.factorial_mul_pow_mul_collapsedCoeff_self and GranvilleMoore.exists_int_factorial_mul_pow_mul_collapsedCoeff_self: the leading value A_j(j) = β_{j,j} p^{C(j,2)} ∏_{s<j}(p^{s+1} - 1), its division-free form, and the resulting congruence j! A_j(j) / p^{C(j,2)} ≡ 1 (mod p).

Implementation notes

The coefficient analysis of GranvilleMoore.CoefficientAnalysis is stated over ℤ, because that is where the c_{j,i}(p) live, while collapsedCoeff is rational. The three private *_rat lemmas at the top of this file are those statements pushed through Int.cast, and they are the only place a cast appears; prod_pow_sub_pow_rat_eq_pow_mul also converts the exponent ∑_{r<j} r into C(j,2).

The valuation is usually stated as the inequality v_p(A_j(m)) ≥ C(j,2) - v_p(m!), and that is le_padicValRat_collapsedCoeff. It carries the side condition A_j(m) ≠ 0, which is not avoidable: padicValRat p 0 = 0 by convention, so the unconditional inequality would assert C(j,2) ≤ v_p(m!) at every pair (j, m) where A_j(m) happens to vanish, and that is false already for j = m = 2 and p odd. The inequality is therefore derived from a sharper, purely algebraic and unconditional form, exists_intCast_eq_factorial_mul_pow_mul_collapsedCoeff, which says that

m! (p-1)^m A_j(m) / p^{C(j,2)}

is an integer. That is the form a consumer wanting integrality should use — it holds for all j and m with no nonvanishing hypothesis and no primality beyond p ≠ 1 in spirit — and the valuation bound follows from it because p ∤ p - 1. Neither statement needs j ≤ m: for j > m the collapsed coefficient vanishes and both are trivially true.

For the leading coefficient the paper asserts the congruence A_j(j)/p^{C(j,2)} ≡ 1/j! (mod p) for j ≤ p - 1. A congruence between rational numbers is not a Mathlib notion, so what is proved here is the exact factorisation that the paper's proof actually establishes, in three increasingly explicit forms:

• collapsedCoeff_self_eq: A_j(j) = β_{j,j} p^{C(j,2)} ∏_{s<j}(p^{s+1} - 1);
• factorial_mul_pow_mul_collapsedCoeff_self: the same with β_{j,j} eliminated using factorial_mul_pow_mul_binomPolyCoeff_self, giving the division-free identity j! (p-1)^j A_j(j) = p^{C(j,2)} ∏_{s<j}(p^{s+1} - 1);
• exists_int_factorial_mul_pow_mul_collapsedCoeff_self: the congruence itself, in the shape j! (p-1)^j A_j(j) = p^{C(j,2)} ((p-1)^j + p a) for an integer a, which says exactly that j! A_j(j)/p^{C(j,2)} differs from 1 by p a/(p-1)^j, a rational of positive valuation.

None of the three needs j ≤ p - 1: that hypothesis exists only to make 1/j! p-integral, i.e. to give the congruence's right-hand side a meaning, and the forms above clear j! instead of inverting it. They need only 2 ≤ p.

Rational forms of the coefficient analysis

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

GranvilleMoore.prod_pow_sub_pow_eq_zero over ℚ.

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

GranvilleMoore.prod_pow_sub_pow_eq_pow_mul over ℚ, with the exponent written as C(j,2).

The closed form

theorem GranvilleMoore.collapsedCoeff_eq_sum {p : ℕ} (hp : 2 ≤ p) (j m : ℕ) : collapsedCoeff p j m = ∑ n ∈ Finset.range (m + 1), binomPolyCoeff p m n * ∏ r ∈ Finset.range j, (↑p ^ n - ↑p ^ r)

lem_A_formula: the collapsed coefficient in closed form, A_j(m) = ∑_{n ≤ m} β_{m,n} ∏_{r<j}(p^n - p^r).

Substituting the expansion C(e_i, m) = ∑_{n ≤ m} β_{m,n} (p^n)^i of GranvilleMoore.natCast_choose_frobeniusExponent_eq_sum into the definition and exchanging the two finite sums leaves, for each n, the signed sum ∑_i (-1)^{j-i} c_{j,i} (p^n)^i, which is ∏_{r<j}(p^n - p^r) by GranvilleMoore.signedCCoeff_sum_eq_prod.

theorem GranvilleMoore.collapsedCoeff_eq_zero {p : ℕ} (hp : 2 ≤ p) {j m : ℕ} (h : m < j) : collapsedCoeff p j m = 0

lem_A_vanishes: the collapsed coefficient vanishes in low degree, A_j(m) = 0 for m < j.

Every index n of the closed form satisfies n ≤ m < j, so every product vanishes by GranvilleMoore.prod_pow_sub_pow_eq_zero.

The valuation

theorem GranvilleMoore.exists_intCast_eq_factorial_mul_pow_mul_collapsedCoeff {p : ℕ} (hp : 2 ≤ p) (j m : ℕ) : ∃ (a : ℤ), ↑m.factorial * (↑p - 1) ^ m * collapsedCoeff p j m = ↑p ^ j.choose 2 * ↑a

lem_A_valuation, algebraic form: m! (p-1)^m A_j(m) / p^{C(j,2)} is an integer.

This is the unconditional content behind the valuation inequality: it exhibits the denominator of A_j(m) explicitly as m! (p-1)^m and its p-power numerator as p^{C(j,2)}. In the closed form every term with n < j vanishes and every term with n ≥ j contributes a factor p^{C(j,2)}.

theorem GranvilleMoore.le_padicValRat_collapsedCoeff {p : ℕ} (hp : Nat.Prime p) {j m : ℕ} (h : collapsedCoeff p j m ≠ 0) : ↑(j.choose 2) - padicValRat p ↑m.factorial ≤ padicValRat p (collapsedCoeff p j m)

lem_A_valuation: v_p(A_j(m)) ≥ C(j,2) - v_p(m!).

Taking p-adic valuations in the algebraic form GranvilleMoore.exists_intCast_eq_factorial_mul_pow_mul_collapsedCoeff: the integer on the right has nonnegative valuation and v_p((p-1)^m) = 0, so v_p(m!) + v_p(A_j(m)) ≥ C(j,2).

The hypothesis A_j(m) ≠ 0 is needed because padicValRat p 0 = 0; a consumer that cannot supply it should use the algebraic form, which has no side condition.

The leading coefficient

theorem GranvilleMoore.factorial_mul_pow_mul_binomPolyCoeff_self {p : ℕ} (hp : p ≠ 1) (m : ℕ) : ↑m.factorial * (↑p - 1) ^ m * binomPolyCoeff p m m = 1

The leading coefficient of B_m: m! (p-1)^m β_{m,m} = 1, i.e. β_{m,m} = 1/(m! (p-1)^m).

Clearing the denominators of B_m turns it into the monic polynomial ∏_{s<m} (X - 1 - s(p-1)) of degree m (GranvilleMoore.C_mul_binomPoly_eq_prod), whose top coefficient is 1.

theorem GranvilleMoore.collapsedCoeff_self_eq {p : ℕ} (hp : 2 ≤ p) (j : ℕ) : collapsedCoeff p j j = binomPolyCoeff p j j * ↑p ^ j.choose 2 * ∏ s ∈ Finset.range j, (↑p ^ (s + 1) - 1)

lem_A_leading, the factorisation: A_j(j) = β_{j,j} p^{C(j,2)} ∏_{s<j}(p^{s+1} - 1).

In the closed form with m = j every term with n < j vanishes, leaving the single term β_{j,j} ∏_{r<j}(p^j - p^r); that product factors as p^{C(j,2)} ∏_{r<j}(p^{j-r} - 1) by GranvilleMoore.prod_pow_sub_pow_eq_pow_mul, and re-indexing by s = j - 1 - r turns the remaining product into ∏_{s<j}(p^{s+1} - 1), each of whose factors is ≡ -1 (mod p).

theorem GranvilleMoore.factorial_mul_pow_mul_collapsedCoeff_self {p : ℕ} (hp : 2 ≤ p) (j : ℕ) : ↑j.factorial * (↑p - 1) ^ j * collapsedCoeff p j j = ↑p ^ j.choose 2 * ∏ s ∈ Finset.range j, (↑p ^ (s + 1) - 1)

lem_A_leading, division-free: j! (p-1)^j A_j(j) = p^{C(j,2)} ∏_{s<j}(p^{s+1} - 1).

The factorisation of GranvilleMoore.collapsedCoeff_self_eq with β_{j,j} eliminated by GranvilleMoore.factorial_mul_pow_mul_binomPolyCoeff_self. Dividing by p^{C(j,2)} and by (p-1)^j this reads A_j(j)/p^{C(j,2)} = (1/j!) ∏_{s<j}(p^{s+1}-1)/(p-1)^j, which is the displayed formula of the paper's proof.

theorem GranvilleMoore.exists_int_factorial_mul_pow_mul_collapsedCoeff_self {p : ℕ} (hp : 2 ≤ p) (j : ℕ) : ∃ (a : ℤ), ↑j.factorial * (↑p - 1) ^ j * collapsedCoeff p j j = ↑p ^ j.choose 2 * ((↑p - 1) ^ j + ↑p * ↑a)

lem_A_leading, the congruence: there is an integer a with j! (p-1)^j A_j(j) = p^{C(j,2)} ((p-1)^j + p a).

Equivalently j! A_j(j)/p^{C(j,2)} = 1 + p a/(p-1)^j, and since p ∤ p - 1 the correction term has positive valuation: this is the congruence A_j(j)/p^{C(j,2)} ≡ 1/j! (mod p), with j! cleared instead of inverted. It comes from the division-free identity together with ∏_{s<j}(p^{s+1} - 1) ≡ (p-1)^j (mod p), both sides being ≡ (-1)^j.