AI 中文总结
本文证明了限制二项式系数最大公因数在素数 p≡-1 mod m 处的完整 p-进赋值公式，利用 Kummer 定理和带符号零和分类，并在 Lean 4 中形式化验证。
AI 中文摘要
对于整数 $m\geq 2$ 且 $m\mid N$，设 $G(N;m)=\gcd\{\binom{N}{k}:0<k<N,\\ m\mid k\}$。我们在假设 $m\geq 3$、$m\mid N$ 且 $m<N$ 下，证明了 $G(N;m)$ 在素数 $p\equiv -1\pmod m$ 处的完整 $p$-进赋值公式。记 $N=\sum_i d_i p^i$，令 $A=\sum_{i\text{ even}}d_i$，$B=\sum_{i\text{ odd}}d_i$。则 $v_p(G(N;m))$ 在例外混合情形 $(A,B)=(1,1)$ 且 $p=m-1$ 时为 $2$，在混合情形 $(A,B)=(1,1)$ 且 $m<p$ 时为 $1$，在单奇偶情形 $(A,B)=(m,0)$ 和 $(A,B)=(0,m)$ 时为 $1$，其余情形为 $0$。证明使用 Kummer 定理将问题转化为逐位借位计数和最小带符号零和分类。截至 2026 年 9 月 25 日的源码级文献审计未发现针对完整负一类分类的等价先前定理：McTague 修正后的同余类扩展覆盖了 $p>m$ 的单奇偶子情形，但不覆盖混合奇偶分支或 $p=m-1$ 情形。该定理、其正一类伴随定理、缩放约化以及 $m=3,4,6$ 的特例已在 Lean 4 / Mathlib 中形式化。
英文摘要
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.
Comments8 pages, no figures. Lean 4 / Mathlib formalization: https://github.com/jfairfaxball-348/pascal-minus-one . Palomar record PALOMAR-2026-09-25-000017, version 1
