Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in math-comp

Definition 1.7Binomial coefficient

The binomial coefficient \(\binom {n}{k}\), written ’C(n, k) in MathComp.

LaTeX Rocq

Definition 2.6Carry

For a base \(p\), position \(i\), and natural numbers \(a, b\), define

\[ \mathrm{carry}(p, i, a, b) \; :=\; [p^i \leq (a \bmod p^i) + (b \bmod p^i)]. \]

This is \(1\) (true) when adding \(a\) and \(b\) produces a carry at position \(i\) in base \(p\).

LaTeX Rocq

Definition 6.1Base-\(p\) digit

For \(p \geq 2\), the \(i\)-th digit of \(n\) in base \(p\) is

\[ d_i(n) := \left\lfloor \frac{n}{p^i} \right\rfloor \bmod p. \]

LaTeX Rocq

Definition 6.4Digit sum

The sum of base-\(p\) digits of \(n\):

\[ s_p(n) := \sum _{i=0}^{\texttt{trunc\_ log}(p,n)} d_i(n). \]

LaTeX Rocq

Definition 1.8Factorial

The factorial \(n!\), written n‘! in MathComp.

LaTeX Rocq

Definition 1.1p-adic valuation

For a prime \(p\) and a natural number \(m\), \(\operatorname {logn}(p, m)\) is the largest \(k\) such that \(p^k\) divides \(m\). In MathComp this is logn p m.

LaTeX Rocq

Definition 1.2Truncated logarithm

For \(p \geq 2\) and \(n \in \mathbb {N}\), \(\texttt{trunc\_ log}(p, n)\) is the largest \(k\) such that \(p^k \leq n\).

LaTeX Rocq

Lemma 1.10Factorial decomposition of binomials

For \(k \leq n\),

\[ \binom {n}{k} \cdot k! \cdot (n-k)! = n!. \]

LaTeX Rocq

Lemma 1.11Positivity of binomial coefficients

\((0 {\lt} \binom {n}{k}) \iff (k \leq n)\).

LaTeX Rocq

Lemma 2.5Carry is a boolean division

For \(m {\gt} 0\),

\[ [m \leq (a \bmod m) + (b \bmod m)] = \left\lfloor \frac{(a \bmod m) + (b \bmod m)}{m} \right\rfloor . \]

(The right-hand side is \(0\) or \(1\).) Proof.

LaTeX Rocq

Lemma 6.2Digit bound

For \(p \geq 2\),

\[ d_i(n) {\lt} p. \]

Proof.

LaTeX Rocq

Lemma 6.3Digit representation

For \(p \geq 2\) and \(n {\gt} 0\),

\[ n = \sum _{i=0}^{\texttt{trunc\_ log}(p,n)} d_i(n) \cdot p^i. \]

Proof.

LaTeX Rocq

Lemma 2.1Floor-division addition identity

Let \(m {\gt} 0\). Then for all \(a, b \in \mathbb {N}\),

\[ \left\lfloor \frac{a+b}{m} \right\rfloor = \left\lfloor \frac{a}{m} \right\rfloor + \left\lfloor \frac{b}{m} \right\rfloor + [m \leq (a \bmod m) + (b \bmod m)] \]

where \([\cdot ]\) denotes the Iverson bracket. Proof. Write \(a = qm + r\) and \(b = q'm + r'\) with \(0 \leq r, r' {\lt} m\). Then \(a + b = (q + q')m + (r + r')\). Since \(0 \leq r + r' {\lt} 2m\), we have \(\lfloor (r+r')/m\rfloor \in \{ 0, 1\} \), and it equals \(1\) exactly when \(r + r' \geq m\).

LaTeX Rocq

Lemma 2.7Division with carry

For \(p {\gt} 0\) and \(k \leq n\),

\[ \left\lfloor \frac{n}{p^i} \right\rfloor = \left\lfloor \frac{k}{p^i} \right\rfloor + \left\lfloor \frac{n-k}{p^i} \right\rfloor + \mathrm{carry}(p, i, k, n-k). \]

Proof. Write \(n = k + (n-k)\) and apply Lemma 2.1 with \(m = p^i\).

LaTeX Rocq

Lemma 2.3Sum of remainders bound

For \(m {\gt} 0\),

\[ (a \bmod m) + (b \bmod m) {\lt} 2m. \]

Proof.

LaTeX Rocq

Lemma 2.4Division of sum of remainders

For \(m {\gt} 0\),

\[ \left\lfloor \frac{(a \bmod m) + (b \bmod m)}{m} \right\rfloor \leq 1. \]

Proof.

LaTeX Rocq

Lemma 1.13Euclidean division

For all \(n, d\),

\[ n = (n \mathbin {/} d) \cdot d + n \bmod d. \]

LaTeX Rocq

Lemma 1.15Small dividend

If \(m {\lt} d\) then \(m \mathbin {/} d = 0\).

LaTeX Rocq

Lemma 3.1Vanishing of large floor divisions

For \(p \geq 2\) and \(i {\gt} \texttt{trunc\_ log}(p, n)\),

\[ \left\lfloor \frac{n}{p^i} \right\rfloor = 0. \]

Proof. By trunc_log_ltn, \(n {\lt} p^{\texttt{trunc\_ log}(p,n)+1} \leq p^i\). Apply divn_small.

LaTeX Rocq

Lemma 1.17Division of sum with multiple

For \(0 {\lt} p\),

\[ (p \cdot q + r) \mathbin {/} p = q + r \mathbin {/} p. \]

LaTeX Rocq

Lemma 1.12Positivity of factorial

\(0 {\lt} n!\) for all \(n\).

LaTeX Rocq

Lemma 6.5Legendre’s formula via digit sums

For prime \(p\) and \(n {\gt} 0\),

\[ (p-1) \cdot v_p(n!) = n - s_p(n). \]

Proof. From the digit representation \(n = \sum _i d_i(n) \cdot p^i\) and Legendre’s formula \(v_p(n!) = \sum _{k \geq 1} \lfloor n/p^k \rfloor \). A telescoping argument gives the result.

LaTeX Rocq

Lemma 5.6\(v_2(n!) {\lt} n\)

For \(n {\gt} 0\),

\[ v_2(n!) {\lt} n. \]

Proof. By Legendre’s formula, \(v_2(n!) = \sum _{k \geq 1} \lfloor n/2^k \rfloor {\lt} n \cdot \sum _{k \geq 1} 2^{-k} = n\).

LaTeX Rocq

Lemma 3.3logn of binomial via factorials

For prime \(p\) and \(k \leq n\),

\[ v_p\! \binom {n}{k} = v_p(n!) - v_p(k!) - v_p((n-k)!). \]

Proof. From \(\binom {n}{k} \cdot k! \cdot (n-k)! = n!\) (Lemma 1.10), apply \(v_p\) to both sides using multiplicativity (Lemma 1.3), noting that all factors are positive by Lemmas 1.11 and 1.12.

LaTeX Rocq

Lemma 5.2Primes larger than \(n\) don’t divide \(\binom {n}{k}\)

For prime \(p\) with \(n {\lt} p\) and \(k \leq n\),

\[ v_p\! \binom {n}{k} = 0. \]

Proof. When \(n {\lt} p\), \(\texttt{trunc\_ log}(p, n) = 0\), so there are no carry positions.

LaTeX Rocq

Lemma 5.3Primes with \(p^2 {\gt} n\) appear at most once

For prime \(p\) with \(p^2 {\gt} n\) and \(k \leq n\),

\[ v_p\! \binom {n}{k} \leq 1. \]

Proof. Since \(p^2 {\gt} n\), \(\texttt{trunc\_ log}(p, n) \leq 1\), so there is at most one carry position.

LaTeX Rocq

Lemma 5.1Upper bound on logn of binomial

For prime \(p\) and \(k \leq n\),

\[ v_p\! \binom {n}{k} \leq \texttt{trunc\_ log}(p, n). \]

Proof. By Kummer’s theorem, \(v_p\binom {n}{k}\) counts carries among at most \(\texttt{trunc\_ log}(p, n)\) positions.

LaTeX Rocq

Lemma 5.5Valuation of \(\binom {p^m}{k}\)

For prime \(p\), \(0 {\lt} k \leq p^m\),

\[ v_p\! \binom {p^m}{k} + v_p(k) = m. \]

Proof. Combine Kummer’s theorem with Lemma 1.4.

LaTeX Rocq

Lemma 3.4logn of binomial via Legendre sums

For prime \(p\), \(k \leq n\), and \(b {\gt} \texttt{trunc\_ log}(p, n)\),

\[ v_p\! \binom {n}{k} = \sum _{i=1}^{b} \left\lfloor \frac{n}{p^i} \right\rfloor - \sum _{i=1}^{b} \left\lfloor \frac{k}{p^i} \right\rfloor - \sum _{i=1}^{b} \left\lfloor \frac{n-k}{p^i} \right\rfloor . \]

Proof. Substitute Lemma 3.2 (applied to \(n\), \(k\), and \(n-k\), all with the same bound \(b\)) into Lemma 3.3.

LaTeX Rocq

Lemma 1.9Legendre’s formula

Let \(p\) be prime and \(n \in \mathbb {N}\). Then

\[ v_p(n!) = \sum _{k=1}^{n} \left\lfloor \frac{n}{p^k} \right\rfloor . \]

LaTeX Rocq

Lemma 3.2Legendre with extended bound

For prime \(p\) and \(b {\gt} \texttt{trunc\_ log}(p, n)\),

\[ v_p(n!) = \sum _{i=1}^{b} \left\lfloor \frac{n}{p^i} \right\rfloor . \]

Proof. By Lemma 1.9, \(v_p(n!) = \sum _{i=1}^{n} \lfloor n/p^i \rfloor \). The extra terms for \(i {\gt} \texttt{trunc\_ log}(p,n)\) vanish by Lemma 3.1.

LaTeX Rocq

Lemma 5.4Lower bound on logn of binomial

For prime \(p\), \(k \leq n\), and \(0 {\lt} k\),

\[ v_p(n) \leq v_p\! \binom {n}{k} + v_p(k). \]

Proof.

LaTeX Rocq

Lemma 1.3Multiplicativity of logn

For prime \(p\) and \(m, n {\gt} 0\),

\[ \operatorname {logn}(p, m \cdot n) = \operatorname {logn}(p, m) + \operatorname {logn}(p, n). \]

LaTeX Rocq

Lemma 1.14Modulus bound

\((n \bmod d {\lt} d) \iff (0 {\lt} d)\).

LaTeX Rocq

Lemma 2.2Modular addition

For \(m {\gt} 0\),

\[ (a + b) \bmod m = ((a \bmod m) + (b \bmod m)) \bmod m. \]

Proof.

LaTeX Rocq

Lemma 1.16Modulus of sum with multiple

\((p \cdot q + r) \bmod p = r \bmod p\).

LaTeX Rocq

Lemma 1.4logn of prime powers

For prime \(p\),

\[ \operatorname {logn}(p, p^n) = n. \]

LaTeX Rocq

Lemma 2.8Summed carry-count identity

For prime \(p\), \(k \leq n\), and \(b {\gt} \texttt{trunc\_ log}(p, n)\),

\[ \sum _{i=1}^{b} \left\lfloor \frac{n}{p^i} \right\rfloor = \sum _{i=1}^{b} \left\lfloor \frac{k}{p^i} \right\rfloor + \sum _{i=1}^{b} \left\lfloor \frac{n-k}{p^i} \right\rfloor + \sum _{i=1}^{b} \mathrm{carry}(p, i, k, n-k). \]

Proof. Apply Lemma 2.7 pointwise for each \(i \in \{ 1, \ldots , b\} \) and use linearity of summation.

LaTeX Rocq

Lemma 1.5Truncated log bounds

For \(p \geq 2\) and \(n {\gt} 0\),

\[ p^{\texttt{trunc\_ log}(p, n)} \leq n {\lt} p^{\texttt{trunc\_ log}(p, n) + 1}. \]

LaTeX Rocq

Lemma 1.6Truncated log upper bound

For \(p \geq 2\) and \(n {\gt} 0\),

\[ n {\lt} p^{\texttt{trunc\_ log}(p, n) + 1}. \]

LaTeX Rocq

Theorem 4.1Kummer’s theorem

Let \(p\) be prime and \(0 \leq k \leq n\). Then

\[ v_p\! \binom {n}{k} = \sum _{i=1}^{b} \mathrm{carry}(p, i, k, n-k), \]

for any \(b {\gt} \texttt{trunc\_ log}(p, n)\). Equivalently, the \(p\)-adic valuation of \(\binom {n}{k}\) equals the number of carries when adding \(k\) and \(n-k\) in base \(p\). Proof. By Lemma 3.4,

By Lemma 2.8, the difference of the three Legendre sums equals the carry count.

LaTeX Rocq

Theorem 4.2Kummer’s theorem — cardinality form

For prime \(p\), \(k \leq n\), and \(b {\gt} \texttt{trunc\_ log}(p, n)\),

\[ v_p\! \binom {n}{k} = \# \bigl\{ i \in \{ 1, \ldots , b\} \; \big|\; \mathrm{carry}(p, i, k, n-k) \bigr\} . \]

Proof. Since \(\mathrm{carry}\) is boolean, summing it over \(\{ 1, \ldots , b\} \) equals the cardinality of the set where it holds.

LaTeX Rocq

Theorem 6.6Kummer’s theorem — digit sum form

For prime \(p\) and \(0 {\lt} k \leq n\),

\[ (p-1) \cdot v_p\! \binom {n}{k} = s_p(k) + s_p(n-k) - s_p(n). \]

Proof. Apply Lemma 6.5 to \(n!\), \(k!\), and \((n-k)!\), then use \(v_p\binom {n}{k} = v_p(n!) - v_p(k!) - v_p((n-k)!)\).

LaTeX Rocq