Restricted Binomial GCDs at Primes Congruent to -1
John Fairfax-Ball
math.NT
Sep 29, 2026 · v1
TL;DR
The minus-one valuation theorem, its plus-one companion, a scaling reduction, and the m=3,4,6 specializations are formalized in Lean 4 with Mathlib.
Abstract
For integers $m\geq 2$ and $m\mid N$, let $G(N;m)=\gcd\{\binom{N}{k}:0<k<N,\ m\mid k\}$. We prove a complete $p$-adic valuation formula for $G(N;m)$ at primes $p\equiv -1\pmod m$, under the hypotheses $m\geq 3$, $m\mid N$, and $m<N$. Writing $N=\sum_i d_i p^i$, put $A=\sum_{i\text{ even}}d_i$ and $B=\sum_{i\text{ odd}}d_i$. Then $v_p(G(N;m))$ is $2$ in the exceptional mixed case $(A,B)=(1,1)$ with $p=m-1$, is $1$ in the mixed case $(A,B)=(1,1)$ with $m<p$, is $1$ in the one-parity cases $(A,B)=(m,0)$ and $(A,B)=(0,m)$, and is $0$ otherwise. The proof uses Kummer's theorem to translate the problem into digitwise borrow counts and a minimal signed zero-sum classification. A source-level literature audit through 25 September 2026 located no equivalent prior theorem for the full minus-one classification: McTague's corrected same-residue extension covers the one-parity $p>m$ subcases, but not the mixed-parity branch or the $p=m-1$ regime. The theorem, its plus-one companion, a scaling reduction, and the $m=3,4,6$ specializations have been formalized in Lean 4 / Mathlib.
Problem
G(N;m) is the gcd of the binomial coefficients C(N,k) with 0<k<N and m dividing k. Its p-adic valuation was known for primes p ≡ 1 (mod m) and for some one-parity cases with p ≡ -1 (mod m). A full classification for primes p ≡ -1 (mod m) was missing, including the mixed-parity branch and the case p = m-1.
Approach
Kummer's theorem turns p-adic valuations of binomial coefficients into counts of base-p borrows. Because p^i ≡ (-1)^i (mod m), the condition m | k becomes a signed zero-sum condition on the even-position and odd-position digit sums. A classification of minimal signed zero-sums leaves only the shapes (1,1), (m,0) and (0,m). Each shape is then analyzed with explicit borrow witnesses, and the results are formalized in Lean 4 / Mathlib together with a scaling reduction.
Results
v_p(G(N;m)) equals 2 when (A,B)=(1,1) and p=m-1, and 1 when (A,B)=(1,1) and m<p. It also equals 1 when (A,B) is (m,0) or (0,m), and 0 in all other cases. The theorem, the plus-one companion, the scaling theorem and the small-modulus specializations are machine-checked in Lean.
| Case | v_p(G(N;m)) |
|---|
| (A,B)=(1,1), p=m-1 | 2 |
| (A,B)=(1,1), m<p | 1 |
| (A,B)=(m,0) or (0,m) | 1 |
| otherwise | 0 |
Minus-one valuation formula (Theorem 1.1)