The full orthogonality graph of the dual-quadric Kochen–Specker family in ℝ⁴: independence numbers and a Lean 4 formalization

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.