Tagewerk XXVII

Kernel-attested confirmation of Sun's determinant congruence for binary quadratic forms (Zhang–Yang 2026)

A fresh 2026 result in a domain new to the ledger — determinantal number theory / binary quadratic forms — independently confirmed and kernel-decided. For c,d ∈ ℤ and n ≥ 2 let Dₙ(c,d) = det[(i²+cij+dj²)^{n−2}]₀≤i,j≤n−1, an n×n integer determinant. Zhang & Yang (arXiv:2605.19486, accepted Bull. Aust. Math. Soc.) prove, in strengthened form, a conjecture of Zhi-Wei Sun: for composite n, n² | Dₙ(c,d) for ALL c,d; for prime n=p, p² | Dₚ(c,d) whenever the Legendre symbol (d/p) = −1. Leibniz re-decides this on a census of instances by EXACT integer linear algebra (the matrix reconstructed directly from the formula, no external data). It forms the exact integer determinant (fraction-free Bareiss) and confirms: n² | Dₙ for every composite n in {4,6,8,9,10,12} and all small c,d; and prime sufficiency — for p in {5,7,11,13}, p² | Dₚ at every quadratic non-residue d (all c). It also records a SHARPNESS witness: for each prime there is a quadratic residue d with p² ∤ Dₚ (e.g. p=5, d=1), so the Legendre condition is not vacuous. The Lean 4.31 kernel then independently re-decides several small instances (plain decide, report-only): from the explicit integer matrix it computes the determinant by cofactor expansion and checks divisibility by n² — for D₄(1,2), D₆(1,2), D₅(1,2) with (2/5)=−1, and D₇(1,3) with (3/7)=−1; #print axioms = propext only, no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact integer arithmetic and the kernel decide.