The reduction ladder

The determinant half of the argument about the Moore determinant: the ladder L 0, L 1, …, L (d-1) of ladderMatrix starts at the Moore matrix, each rung costs one power p ^ C(d - i, 2) of p, and the total cost is p ^ C(d + 1, 3).

Main results

• GranvilleMoore.iteratedFermatQuot_sub_iteratedFermatQuot: the row difference identity F⁽ᵃ⁾_(b+1)(x) - F⁽ᵃ⁾_b(x) = p^(b+1) F⁽ᵃ⁺¹⁾_b(x).
• GranvilleMoore.ladderMatrix_zero: L 0 is the Moore matrix, viewed over ℚ.
• GranvilleMoore.ladderMatrix_last_apply: every row of L (d-1) sits at subscript 0.
• GranvilleMoore.det_ladderMatrix_step: one rung, det (L i) = p^C(d-i,2) det (L (i+1)).
• GranvilleMoore.det_mooreMatrix_eq_pow_mul_det_ladderMatrix: the factorisation det M = p^C(d+1,3) det (L (d-1)).

Implementation notes

The row operations of one rung run for b = d-2-i down to 0, so that each row is modified only after it has served as the subtrahend. The bookkeeping is carried here by GranvilleMoore.ladderStep p x i m, the matrix in which exactly the rows at index ≥ m + i + 1 have already been replaced; ladderStep p x i (d-1-i) is L i, one determinant-preserving row operation takes ladderStep p x i (m+1) to ladderStep p x i m, and ladderStep p x i 0 is a row rescaling of L (i+1). Making the set of finished rows explicit is what removes the need to reason about the order of the operations at all: each single step is a Matrix.updateRow whose subtrahend row is visibly untouched.

The d - 1 - i scalars are extracted in one go with Matrix.det_mul_column (which scales rows, despite the name) rather than by Matrix.det_updateRow_smul once per row.

None of the results below needs the bounds d ≥ 2 and i ≤ d - 2: for d ≤ i + 1 the ladder has stabilised, L i = L (i+1), and C(d-i,2) = 0, so one rung is an identity there too. Only p ≠ 0 is genuinely needed, to divide in the recursion for iteratedFermatQuot.

References

• A. Granville, The p-divisibility of the integer Moore determinant and iterated Fermat quotients.

The row difference identity

theorem GranvilleMoore.iteratedFermatQuot_sub_iteratedFermatQuot {p : ℕ} (hp : p ≠ 0) (a b : ℕ) (x : ℤ) : iteratedFermatQuot p a (b + 1) x - iteratedFermatQuot p a b x = ↑p ^ (b + 1) * iteratedFermatQuot p (a + 1) b x

The row difference identity (lem_row_difference): the recursion defining iteratedFermatQuot, cleared of its denominator. Raising the subscript by one changes F⁽ᵃ⁾ by p^(b+1) times the next F⁽ᵃ⁺¹⁾.

The two ends of the ladder

theorem GranvilleMoore.ladderMatrix_zero {d : ℕ} (p : ℕ) (x : Fin d → ℤ) : ladderMatrix p x 0 = (mooreMatrix p x).map fun (z : ℤ) => ↑z

The ladder starts at the Moore matrix (lem_ladder_start): the rows of L 0 are F⁽⁰⁾_0, …, F⁽⁰⁾_(d-1), and F⁽⁰⁾_k(x) = x^(p^k) is the Moore matrix entry. The comparison is stated over ℚ, where the ladder lives, so the integer Moore matrix appears through its entrywise image.

theorem GranvilleMoore.ladderMatrix_last_apply {d : ℕ} (p : ℕ) (x : Fin d → ℤ) (r j : Fin d) : ladderMatrix p x (d - 1) r j = iteratedFermatQuot p (↑r) 0 (x j)

Entries of the last ladder matrix (lem_ladder_last_entries): at the last rung the trailing block of growing subscripts is empty, so the row at index r of L (d-1) is F⁽ʳ⁾_0.

The row operations of one rung

The scalars extracted from one rung

One rung of the ladder

theorem GranvilleMoore.det_ladderMatrix_step {d p : ℕ} (hp : p ≠ 0) (x : Fin d → ℤ) (i : ℕ) : (ladderMatrix p x i).det = ↑p ^ (d - i).choose 2 * (ladderMatrix p x (i + 1)).det

One rung of the ladder (lem_ladder_step): passing from L i to L (i+1) costs exactly p^C(d-i,2).

This is usually stated for d ≥ 2 and i ≤ d - 2; no such bound is needed, since for d ≤ i + 1 both sides read det (L i) = det (L i).

Factoring the Moore determinant

theorem GranvilleMoore.sum_range_sub_choose_two (n : ℕ) : ∑ i ∈ Finset.range (n - 1), (n - i).choose 2 = (n + 1).choose 3

The ladder exponent (lem_ladder_exponent): ∑_{i<n-1} C(n-i,2) = C(n+1,3).

This is the total power of p that the ladder extracts: rung i contributes C(n-i,2). It follows from the hockey stick GranvilleMoore.sum_range_choose_two by the re-indexing c = n - i; the two terms C(1,2) and C(0,2) that the reflected range adds both vanish.

theorem GranvilleMoore.det_mooreMatrix_eq_pow_mul_det_ladderMatrix {d p : ℕ} (hp : p ≠ 0) (x : Fin d → ℤ) : ↑(mooreMatrix p x).det = ↑p ^ (d + 1).choose 3 * (ladderMatrix p x (d - 1)).det

Factoring the Moore determinant (lem_det_factor): the Moore determinant is p^C(d+1,3) times the determinant of the last matrix of the ladder.

ladderMatrix_zero identifies L 0 with the Moore matrix over ℚ, det_ladderMatrix_step supplies the d - 1 rungs, and the exponents add up to C(d+1,3) by sum_range_choose_two. For d = 0 and d = 1 there are no rungs and the exponent is 0, so the identity is an equality of the two ends.