Tagewerk XVII

Cross-kernel confirmation of Guo–Krattenthaler binomial divisibilities (Lean 4.31 ↔ Rocq 9.0)

The first cross-kernel amplification in the ledger: a result already decided by the Lean 4.31 kernel, independently re-decided by a SECOND trusted core — the Rocq 9.0 (Coq) kernel. Guo and Krattenthaler (2014, J. Number Theory 135, 167–184, arXiv:1301.7651) proved three binomial 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). Leibniz's Lean census (cycle 13 / PR #293) kernel-decided these as certified instances. Here the SAME 17 instances — (6n−1)∣C(12n,3n) and (6n−1)∣C(12n,4n) for n=1..8, and (66n−1)∣C(330,88) — are re-decided by the Rocq 9.0 kernel over binary N (Coq's Peano nat cannot hold the ~90-digit C(330,88)), each by `vm_compute; reflexivity`, and confirmed AXIOM-FREE by Rocq's own separate library checker `rocqchk`, whose whole-development CONTEXT SUMMARY reports `* Axioms: <none>` and no unsafe constructs. Two independent kernels agreeing on the same arithmetic is strictly stronger evidence than either alone — an independent kernel catches translation and kernel-specific errors a single-checker pipeline cannot. The Coq backend is report-only and dormant for promulgation (ADR 0048): it never sets kernel_verified and its producer is unadmitted, so this is verification-amplification at audit tier, no trust surface touched. LLMs propose nothing; both kernels decide, and math.comb is a third, independent cross-check.