← All papers
First page of The Four-Qubit Hyperbolic Quadric Has Contextuality Degree 315

The Four-Qubit Hyperbolic Quadric Has Contextuality Degree 315

Zhengyu Li, Amandeep Gupta, Vijay Ganesh

quant-ph Oct 19, 2026 · v1
The contextuality degree 315 theorem for the real four-qubit hyperbolic quadric is formalized and kernel-checked in Lean 4 with Mathlib, using generated data files and kernel evaluations.
The contextuality degree of a set of Pauli contexts is the least number of contexts that every noncontextual $\pm1$ assignment violates. For the four-qubit hyperbolic quadric $\mathcal{Q}^{+}(7,2)$, with $135$ points and $1575$ lines as contexts, Muller et al. conjectured from heuristic searches that the degree is $315$ and that the violated contexts of every optimal assignment form a dual polar space $DW(5,2)$. We prove both conjectures. The lower bound has a short proof by hand: every doily ($GQ(2,2)$) of the quadric contains ten Peres-Mermin grids covering each of its lines four times, so every assignment violates at least three of its fifteen lines, and averaging over the doilies gives $1575/5=315$. The equality case is local: an assignment is optimal exactly when it violates one ruling of one grid in every doily. Using this as a SAT encoding, we show that there are exactly $240$ optimal violated sets, one orbit of $\mathrm{O}^+(8,2)$, each isomorphic to $DW(5,2)$. The same argument gives the first lower bounds $\lceil L/5\rceil$ for all quadrics with $L$ lines in $N\ge4$ qubits. The degree theorem is kernel-checked in Lean 4, and the completeness of the enumeration is certified by a DRAT proof checked by the verified checker cake_lpr.

The contextuality degree of a set of Pauli contexts is the least number of contexts every noncontextual ±1 assignment violates. For the four-qubit hyperbolic quadric Q+(7,2), with 135 points and 1575 lines, Muller et al. conjectured that the degree is 315 and that the violated sets of optimal assignments form a dual polar space DW(5,2).

Every doily (GQ(2,2)) of the quadric contains ten Peres–Mermin grids covering each line four times, so each doily has at least three violated lines. Averaging over doilies gives the lower bound 1575/5 = 315, and an explicit assignment attains it. The equality condition yields a local SAT encoding that enumerates all optima, with the final unsatisfiability certified by a DRAT proof checked by cake_lpr. The degree theorem is formalized in Lean 4 with Mathlib, with generated data files and about 191 kernel evaluations restructured to fit in 2.2 GB of memory.

The degree is exactly 315. There are exactly 240 optimal violated sets, forming one O+(8,2) orbit, each isomorphic to DW(5,2), realized by 61,440 optimal assignments. The same argument gives lower bounds ⌈L/5⌉ for all quadrics in N≥3 qubits. A noncontextuality inequality with exact classical bound 945 versus the quantum value 1575 follows.

Nconfigurationlines L⌈L/5⌉known value / upper bound
3W(5,2)31563=63
4Q+(7,2)1575315=315 (Thm 11)
4Q-(7,2)1071215≤315
4W(7,2)53551071≤1575
5Q+(9,2)237154743≤6975
Doily lower bound versus known values (excerpt of Table 1)