In the Kochen–Specker system of the E8 root system (120 rays, 2025 orthonormal bases), the largest number of bases containing exactly one selected ray is 1680, so every selection fails at least 345 bases. Every maximizer selects 14 rays whose orthogonality graph is seven disjoint edges; there are exactly 1080 maximizers, one for each antipodal pair of norm-4 vectors z of the E8 lattice (the rays r with |⟨r,z⟩| = 2). The proof combines a symmetry-reduced degree-4 Boolean moment relaxation with exact rational dual certificates, a certificate excluding induced three-vertex paths at the optimum, and a classification in the mod-2 quadratic space of E8. The upper bound, the classification, the certificates and two checking programs were produced with a GPT-based AI assistant in one session; these two programs are not independent review. An AI referee then checked that proof with its own code and reproduced every bound exactly. The certificate data are committed by SHA-256. Status: computer-assisted; exact rational certificates; AI-refereed (same model family as the coordinating assistant); not formally verified; not peer reviewed.
In the Kochen–Specker system of the E8 root system (120 rays, 2025 orthonormal bases), the largest number of bases containing exactly one selected ray is 1680, so every selection fails at least 345 bases. Every maximizer selects 14 rays whose orthogonality graph is seven disjoint edges; there are exactly 1080 maximizers, one for each antipodal pair of norm-4 vectors z of the E8 lattice (the rays r with |⟨r,z⟩| = 2). The proof combines a symmetry-reduced degree-4 Boolean moment relaxation with exact rational dual certificates, a certificate excluding induced three-vertex paths at the optimum, and a classification in the mod-2 quadratic space of E8. The upper bound, the classification, the certificates and two checking programs were produced with a GPT-based AI assistant in one session; these two programs are not independent review. An AI referee then checked that proof with its own code and reproduced every bound exactly. The certificate data are committed by SHA-256. Status: computer-assisted; exact rational certificates; AI-refereed (same model family as the coordinating assistant); not formally verified; not peer reviewed.
The 60 complex rays and 105 orthonormal bases arising from the two-qubit Pauli group form the Kochen-Specker system of Waegell and Aravind (2011), recently named by Aravind, Burton, Nunez Ponasso and Richter (2026) as a natural target for symmetry-based analysis. This note determines exactly the largest number of the 105 bases satisfiable by a single {0,1} ray assignment: the answer is 93, so at least twelve bases must fail. The optimum has clean structure: an attaining assignment selects exactly one state from each of the fifteen maximal abelian subgroups of the Pauli group, so all fifteen stabilizer bases are satisfied and all twelve failures are hybrid bases. The bound is certified by two independent integer-programming solvers (CBC proven optimum; HiGHS optimality and infeasibility of 94), and the attaining assignment is re-verified in exact Gaussian-integer arithmetic. The tight inequality is 93 versus the quantum value 105 (ratio 35/27 in the +/-1 normalization). This is the exact two-qubit analog of the value 65 of 75 determined by the author for the 600-cell system. Verification: run python3 verify2q.py with rays60c.txt in the same directory; it rebuilds the system from the fixed data and re-verifies the anchors (60 rays, 105 bases, seven per ray), the certificate count of 93, the transversal property, and the twelve failing bases in seconds, without any solver.
The 60 rays and 75 orthonormal bases derived from the vertices of the 600-cell form the well-known Kochen-Specker system of Waegell and Aravind. This note determines exactly the largest number of the 75 bases that a single {0,1} ray assignment can satisfy (exactly one ray valued 1 per satisfied basis): the answer is 65, so at least ten bases must fail. This improves the lower bound of nine failures obtained by Waegell, Aravind, Megill and Pavicic (2011) from parity-proof coverings, answers the question they left open, and settles the corresponding open problem restated by Aravind, Burton, Nunez Ponasso and Richter (2026) for the 600-cell. The lower bound is an explicit 17-ray assignment verified in exact Q(sqrt5) arithmetic; the upper bound is certified both by two independent integer-programming solvers and by an explicit family of 150 parity proofs (ten orbits under the triacontagonal C15 symmetry) admitting no nine-element hitting set. The tight noncontextuality inequality is 65 versus the quantum value 75 (ratio 15/11 in the +/-1 normalization). A transfer proposition brackets the analogous 120-cell maximum in [600, 625]. Verification: run python3 verify.py with proofs150.txt in the same directory. It rebuilds the system from the two stated generators and re-verifies the construction anchors, the certificate count of 65, the ten failing bases, and the validity of all 150 parity proofs in seconds, without any solver.
The best known lower bound for the minimum Kochen-Specker vector system in R3 -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.
The 300 rays and 675 orthonormal bases of the 120-cell form the Kochen-Specker system of Waegell and Aravind. This note determines exactly the largest number of the 675 bases satisfiable by a single {0,1} ray assignment (exactly one ray valued 1 per satisfied basis): the answer is 600, so at least seventy-five bases must fail. The proof avoids the intractable full-system optimization entirely: left and right multiplication by the binary icosahedral group partition the rays into five left and five right blocks, each an isometric copy of the 600-cell system; a single 60-ray integer program, proven optimal and transported to all ten blocks by the icosian symmetry, gives the per-block frontier 2*(block-only satisfied) + (doubly satisfied) <= 120; summing over each partition double-counts the doubly embedded bases and collapses the bound to 600. An explicit assignment attains 600. This improves the transfer bracket [600, 625] of DOI 10.5281/zenodo.21249805 to an exact value and closes the third member of the open family of Aravind, Burton, Nunez Ponasso and Richter. Whether parity proofs alone force the bound (as they provably do for the 600-cell and the two-qubit system) is posed as the sharpened open question: the argument gives hitting number h <= 75, and h = 75 remains to be decided. Verification: run python3 verify_max600.py with rays300.txt in the same directory. Structural checks are instant; the two 60-ray integer programs finish in minutes; no full-system optimization is used anywhere.
The 240 root vectors of the Lie algebra E8 lead to a system of 120 rays in a real eight-dimensional Hilbert space that contains a large number of parity proofs of the Kochen–Specker (KS) theorem. After introducing the rays in a triacontagonal representation due to Coxeter, we present their KS diagram in the form of a 'basis table' showing all 2025 bases (i.e., sets of eight mutually orthogonal rays) formed by the rays. Only a few of the bases are actually listed, but simple rules are given, based on the symmetries of E8, for obtaining all the other bases from the ones shown. The basis table is an object of great interest because all the parity proofs of E8 can be exhibited as subsets of it. We show how the triacontagonal representation of E8 facilitates the identification of substructures that are more easily searched for their parity proofs. We have found hundreds of different types of parity proofs, ranging from 9 bases (or contexts) at the low end to 35 bases at the high end, and involving projectors of various ranks and multiplicities. After giving an overview of the proofs we found, we present a few concrete examples of the proofs that illustrate both their generic features as well as some of their more unusual properties. In particular, we present a proof involving 34 rays and 9 bases that appears to provide the most compact proof of the KS theorem found to date in eight-dimensions.
We study the orthogonality graphs Gn of the Kochen–Specker configurations Zn,n(kn, kn) recently obtained by Favacchio from grids on dual quadrics: for every odd n ≥ 3 they consist of 2n2 rays in R4 and n2 orthogonal bases, and G3 is the 18-ray set of Cabello, Estebaranz and García-Alcaine. We determine all orthogonal pairs, not only those inside the bases: Gn is (2n + 1)-regular, and the “only if” direction rests on the fact that 2 cos(2πt/n) is a unit in the ring of algebraic integers for odd n and t ̸≡ 0, while 2 is not. Consequently the independence number is α(Gn) = (n2 − 1)/2, with an explicit maximum independent set, whereas ϑ(Gn) = α∗(Gn) = n2/2 by the standard argument of Cabello, Severini and Winter (CSW). Through the CSW correspondence, every member thus gives a state-independent noncontextuality inequality with classical bound (n2−1)/2 and quantum value n2/2. The list of orthogonal pairs, α, α∗ and the value of Lovász’s max-characterization of ϑ are formalized in Lean 4 with Mathlib, for the rays given by explicit coordinates.