Tagewerk XXXIV

Kernel-attested Simplest Kochen-Specker Set: a 14-basis KS set refuting a 2025 PRL conjecture (Cabello 2025)

A 2025 disproof of a published conjecture in a domain new to the ledger — quantum contextuality / Kochen-Specker sets — independently re-decided and fully kernel-attested. A Kochen-Specker (KS) set is a finite set of vectors admitting no {0,1}-assignment f with f(u)+f(v)<=1 for orthogonal u,v and sum=1 over each orthonormal basis. Cabello (PRL 135, 190203, 2025; arXiv:2508.07335) exhibits a KS set of 33 qutrit vectors using only 14 orthogonal bases -- a record-low number of bases (previous record 16, Peres) -- refuting Conjecture 2 of PRL 134, 010201 (2025) on the minimum number of inputs. The vectors have Eisenstein-integer components (w=e^{2 pi i/3}, w^2=-1-w); the 14 bases are Eqs (1a)-(1e), (2a)-(2i). Leibniz re-decides both halves by exact arithmetic over Z[w]: each of the 14 printed bases is mutually orthogonal (Hermitian inner product 0) and the vectors span exactly 33 distinct rays; and the set is KS-uncolorable -- no {0,1}-assignment with exactly-one per basis and at-most-one per orthogonal edge exists, a finite UNSAT verified by a bounded backtracking search (~1.2k nodes; also confirmed unsat by z3). Reproducing basis orthogonality caught one text-extraction artifact (the x=3 third vector is (w^2,-w,1), a dropped minus sign). The Lean 4.31 kernel re-decides basis orthogonality and uncolorability directly (exact Z[w] arithmetic; the backtracking solver in-kernel -- no external SAT/DRAT dump), plus a negative control (a 13-basis subset is colorable). With 14 bases this beats the previous record of 16, refuting the minimum-inputs conjecture. #print axioms at most [propext]; no native_decide, no sorry. Report-only, audit tier -- the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact arithmetic and the kernel decide.