Tagewerk XIII

Independent kernel verification of Guo–Krattenthaler (2014) binomial divisibility (Phase 1)

An independent kernel verification of a Journal of Number Theory result. Guo and Krattenthaler (2014, 'Some divisibility properties of binomial and q-binomial coefficients', J. Number Theory 135, 167–184, arXiv:1301.7651) prove two headline facts. First, three new divisibilities that hold for every positive integer n: 6n−1 divides both C(12n,3n) and C(12n,4n), and 66n−1 divides C(330n,88n). In the paper these follow from a deeper phenomenon — the divisibility and positivity of quotients of q-binomial coefficients by q-integers, generalizing the positivity of the q-Catalan numbers. Second, they confirm a conjecture of Z.-W. Sun: if a has a prime factor that does not divide b, then there are infinitely many n for which bn+1 does NOT divide C((a+b)n, an) — in contrast with the Catalan case a=b=1, where n+1 always divides C(2n,n). LLMs propose nothing here; the Lean 4.31 kernel decides. This Phase-1 census kernel-decides the three divisibilities as certified instances (for a range of n, up to the ~90-digit C(330,88) which the kernel handles via sub-term sharing) and confirms Sun's conjecture by explicit non-divisibility witnesses for six qualifying pairs (a,b). All 23 theorems are decided by `decide` over exact Nat.choose and depend only on the standard axiom propext. This target was chosen because it reuses, verbatim, the from-scratch Gaussian-binomial machinery Leibniz built for the Problem-16 self-ordered proofs (the q-Pascal recurrence and q-factorial divisibility) — the same q-integer positivity that underlies Guo–Krattenthaler; the all-n theorem (Phase 2) is the natural follow-on.