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.
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.
We develop a geometric framework for constructing and organizing Kochen--Specker configurations in real four-dimensional space. The construction uses finite grids on pairs of smooth quadrics related by Euclidean polarity. Their incidence geometry directly produces orthogonal measurement contexts and parity proofs of quantum contextuality, yielding infinite families of configurations and a geometric interpretation and extension of a previously known cyclic construction. For a distinguished subfamily, the same geometry admits a canonical completion determined by secant lines. The first two instances of this completion recover the exceptional root configurations of types F4 and H4, while the smallest case also recovers the Cabello configuration and its embedding in the Peres configuration. Thus several prominent four-dimensional contextual configurations, previously obtained from different constructions, arise from a single projective-geometric mechanism.
We look at generalisations of sets of vectors proving the Kochen-Specker theorem in 3 and 4 dimensions. It has been shown that two such sets, although unitarily inequivalent, are part of a larger 3-parameter family of vectors that share the same orthogonality graph. We find that these sets are unusual, in that the vectors in all other Kochen-Specker sets investigated here are fully determined by orthog-onality conditions and thus admit no free parameters. The Kochen-Specker (KS) theorem [1] is a statement about the fundamen-tal nature of quantum mechanics: no non-contextual hidden variable theory can reliably reproduce quantum mechanical predictions. The KS theorem states that in a Hilbert space with dimension n ≥ 3 it is impossible to assign definite values v ∈ {0, 1} to m projection operators Pm so that for every commuting set of projection operators satisfying Pm = I, the correspond-ing definite values obey v (Pm) = 1. The KS theorem is often visualised by means of a set of "uncolourable" vectors, where projection operators are represented by their constituent rays in Hilbert space and rays can be simplified to vectors as only directions are relevant here. The vectors are coloured according to their pre-assigned val-ues and the summation conditions above translate into colouring rules. This allows us to construct orthogonality graphs that, when uncolourable, pro-vide a contradiction within non-contextual hidden variable models and thus a proof of the KS theorem. Sets of vectors exemplifying the KS theorem have been discovered by nu-merous authors, with an aim to reduce the number of vectors required to reach a contradiction. Most notably, in a 3-dimensional Hilbert space, the original KS proof of 117 vectors has been replicated with sets using between 31 and 33 vectors [2, 3, 4, 5] and in a 4-dimensional Hilbert space, sets of between 24 and the lower limit of 18 vectors have been realised [2, 6, 7]. Additionally, an extensive computer search has recently revealed over one thousand of such KS sets in R4 [8]. In a publication by E. Gould and P. K. Aravind [10], two of these sets in 3 dimensions have been shown to share the same orthogonality graph. Specifically, the sets of 33 vectors found by Penrose [3] and Peres [2] have
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.
We give a constructive analysis of Kochen-Specker (KS) contextuality at the level of complete orthogonal bases (contexts). In dimension three, three noncomputational mutually unbiased bases generate a union of 165 rays and 130 contexts. Exact provenance accounting gives a symmetric decomposition: the three 69-ray lineages share 21 rays and 10 contexts, while each contributes 48 exclusive rays and 40 lineage-specific contexts. Each 69-ray, 50-context lineage is a KS configuration, and this framework clarifies the relation among the Yu-Oh, Harding-Salinas Schmeis, and Cabello constructions. In dimensions four and five, we give parametrized orthogonality gadgets whose connector contexts force a central ray to be maximally unbiased relative to the computational basis. For the concrete four-dimensional example, the 20-ray gadget and the Cabello 18-ray set are informationally equivalent subsets of the 24-ray Peres-Mermin eigensystem, although their context hypergraphs have different two-valued-state behavior. The results show why both the rays and the complete incidence structure of their contexts are needed in assessments of KS contextuality.
For the regular odd KCBS n-cycle of qutrit projectors under white noise, E ↦ (1−η)E + ηI/3, let η_KS(n) be the least noise at which the noisy effects admit a joint measurement whose outcomes are the Kochen–Specker (KS) value assignments of the cycle, i.e. its independent sets. The dihedral symmetry reduces the semidefinite program over the ≈ 1.6^n independent sets to a second-order cone program on the orbits of arcs (runs of physically consecutive rays), whose data are Dirichlet kernels; its value η_arc(n) is an upper bound. We prove the arc lemma η_KS(n) = η_arc(n) for every odd n ≥ 5. The proof combines a combinatorial lemma — for weights b0 + b1 cos φ + b2 cos²φ with b2 ≤ 0 a minimum-weight independent set of the cycle is an arc — proved on paper and, independently, in Lean 4, with a computer-assisted certificate, in ball arithmetic, of the sign of y2 − y1 for all n. Comparing the discrete problem with its relaxation in which the arc length is a continuous parameter (value η_s(n)) we prove the sandwich η_s(n) ≤ η_KS(n) ≤ η_s(n) + C t(1−t)/n², t = frac(n ρ1(n)), for all odd n ≥ 7, with C ≤ 3.55 for n ≥ 401 (direct construction; the Lagrangian bound gives 3.59). As a consequence η_KS(n) → η_∞ = 0.42473994622455799193…, the value of an explicit continuum problem, and the rounding constant tends to c_∞ = 3.47856584115611146…, with a rate (computer-assisted): |η_KS(n) − η_s(n) − c_∞ t(1−t)/n²| ≤ 1.97/n³ for all odd n ≥ 7, and with an explicit second term. The thresholds are not monotone (computer-assisted): η_KS(n+2) > η_KS(n) and η_KS(n+2) < η_KS(n) each for infinitely many n, with approximate period 4 and a slow beat. For 5 ≤ n ≤ 401 and five larger n the thresholds are enclosed to 10^−35 as roots of explicit algebraic systems. A parameter-free form of the rounding law, fixed by a recorded hash before the corresponding discrete values were read, predicted the optimal support for 60 of 60 values 83 ≤ n ≤ 201.
Observable-based Kochen-Specker proofs are configurations of multi-qubit Pauli observables grouped into contexts whose products are plus or minus the indentity. Their robustness as state-independent contextuality tests can be measured by the tolerated error per context ε=2d/∣H∣, where d is the contextuality degree and ∣H∣ the number of contexts. Since the degree depends only on an underlying abstract structure called the hypergram i.e. the pair formed by the context hypergraph and the anticommutation graph, the search for highly contextual proofs can be carried out on them instead, with no reference to qubits or to any particular Pauli labeling. We further exploit this by enumerating anticommutation graphs first, and then by associating to each graph G the single hypergram carrying its entire hypergraph support HS(G), so that exactly one candidate is examined per graph. Applied to the House of Graphs database and to censuses of vertex-transitive graphs on at most 24 vertices, this pipeline recovers the Peres-Mermin square, the doily and the Mermin pentagram, and yields configurations reaching ε=0.707, against 0.424 for the previous published record. The best configurations are predominantly those stemming from line graphs and unions of graphs; we explain the former by showing that every perfect matching of a graph is a context of its line graph, which exhibits the Peres-Mermin square and the doily as the first members of two infinite families. We close with finite geometric descriptions of the most striking configurations inside symplectic polar spaces, in terms of ovoids, hyperbolic quadrics and Fano planes.