The Four-Qubit Hyperbolic Quadric Has Contextuality Degree 315

Introduction

The Kochen–Specker theorem [33, 6] rules out noncontextual hidden-variable models of quantum mechanics: there is no assignment of definite values to observables, independent of which compatible observables are measured alongside, that respects the functional relations quantum mechanics imposes on every set of commuting observables. The most transparent proofs use Pauli observables. In the Peres–Mermin square [46, 38, 39] nine two-qubit Pauli observables are arranged in a $3 \times3$ grid whose rows and columns are triples of commuting observables with product $+I$, except for one column with product $-I$. No assignment of $\pm1$ values satisfies all six constraints. Such state-independent proofs underlie experimental tests of contextuality [11, 31, 3] and connect contextuality to the power of quantum computation [48, 28].

The non-identity $N$-qubit Pauli observables, taken up to sign, are the points of the symplectic polar space $W(2N - 1, 2)$ of rank $N$ over $\mathbb{F}_{2}$, two observables commuting exactly when the corresponding points are orthogonal [53, 20, 58]. This dictionary has made finite geometry a natural language for observable-based contextuality [26, 60, 34, 52]. Any family of totally isotropic lines, each line $\{A,B,AB\}$ carrying the sign of $A \cdot B = \pm I$, defines a candidate contextuality configuration. De Boutray, Holweck, Giorgetti, Masson and Saniga [13] introduced the contextuality degree, the least number of contexts that a noncontextual assignment must violate, as a measure of how contextual such a configuration is. It governs both the classical bound of the associated noncontextuality inequality [12, 30] and the classical winning probability of the associated Mermin-type games [4, 30]. Computing it is a MAX-XOR-SAT problem, and exact values are known only for small configurations: the doily (3), the three-qubit space $W(5, 2)$ (63) and its quadrics (21 and 9) [13, 42, 50].

For four qubits the problem has resisted computation. The hyperbolic quadric $Q^{+}(7, 2)$ has 135 points and 1575 lines. Muller, Saniga, Giorgetti, de Boutray and Holweck [43, Table 1] could only show that its degree is at most 500. Muller, Saniga, Giorgetti, Holweck and Kelleher {citep}[44 §5.1.2] then found, with a heuristic search, assignments violating only 315 lines, observed that the 315 unsatisfied lines are isomorphic to the dual polar space $DW(5, 2)$, and wrote: “So, we do believe that $d^{\mathrm{hyp}}_4 = 315$, with the understanding that the corresponding unsatisfied configurations are (always) isomorphic to $DW(5, 2)$.” Saniga, Holweck, Kelleher, Muller, Giorgetti and de Boutray {citep}[50 p. 24] single out a closely related question as “computationally rather challenging”, whose affirmative answer “would mean, among other things, that the degree of contextuality of a four-qubit hyperbolic quadric is 315”. Muller and Giorgetti {citep}[41 §5.3] and Muller’s thesis {citep}[40]` list 315 as an upper bound only.

Results. We settle both parts of this conjecture.

• Theorem 11. Every hyperbolic quadric of the four-qubit space, with its 1575 lines as contexts, has contextuality degree exactly 315.

• Proposition 14 and Theorem 15. In every optimal assignment, each of the 40 320 doilies of the quadric has exactly three violated lines, which form one ruling of one of its grids. There are exactly 240 sets of lines that arise as the violated set of an optimal assignment; they form one orbit of the orthogonal group $O^{+}(8, 2)$, and each is isomorphic to $DW(5, 2)$. The first statement has a short proof by hand; the second is computer-assisted.

• Theorem 17. For every $N \ge3$, every hyperbolic or elliptic quadric of the $N$-qubit space, with $L$ lines, has degree at least $\lceil L/5\rceil$. This is tight for $N = 3$ and for the four-qubit hyperbolic quadric, and to our knowledge it gives the first lower bounds for the elliptic four-qubit quadric and for all quadrics with $N \ge5$ qubits.

• Corollary 18. The 1575 contexts give a state-independent noncontextuality inequality with classical bound exactly 945 and quantum value 1575; equivalently, a uniformly random context is satisfied with probability at most $4/5$ by any noncontextual assignment, and this bound is attained.

The proof of the lower bound is short and needs no computation, and we regard this as its main point: a value that resisted solver-based attacks follows from three classical ingredients. These are the parity argument behind the Peres–Mermin square; Sylvester’s model of the generalised quadrangle $GQ(2, 2)$, which shows that a doily contains ten grids covering each of its lines four times; and Witt’s theorem, which makes the orthogonal group transitive on the lines of the quadric. The averaging principle itself is not new. Saniga et al. [50 §4.1] obtained the degree 63 of $W(5, 2)$ by averaging over its doilies, and Muller et al. [44 §4] bounded the degree of the whole space $W(2N - 1, 2)$ by a recursion over subspaces; as far as we know, it had not been applied to the quadrics, where it turns out to be tight. The rounding $\lfloor10/4\rfloor= 3$ inside each doily is what makes the bound tight: averaging over the 67 200 grids of the quadric directly gives only $\lfloor1575/6\rfloor= 263$. What we regard as the main new content is what the equality case gives: a local characterisation of all optimal assignments (Proposition 14), which turns the classification of the optima into an easy and certified computation (Theorem 15), together with a formal proof of the degree.

We formalised the theorem for the real quadric (the observables with an even number of $Y$ factors) in Lean 4 with Mathlib [15, 59]; the kernel checks every finite fact, and the statement depends only on the standard axioms (§ 9). All code and certificates are available at https://github.com/BrianLi009/four-qubit-hyperbolic-quadric.

For the formal-methods reader. Computing a contextuality degree is a MAX-XOR-SAT problem, here with 135 variables and 1575 parity constraints of length three, and this one had resisted the solver-based attacks of [43, 44]. SAT solving has settled several open problems in combinatorics, often with the help of mathematical insight in the encoding [22, 65]. The present case is an extreme instance of that pattern: the mathematics settles the optimisation problem completely, and what remains for the solver, the classification of all optima, becomes easy only after the proof is turned into constraints. Sections 10.2 and 10.3 give the encoding and a comparison: direct MaxSAT and cardinality formulations do not finish within 30 minutes, while local cardinality constraints over doilies, together with redundant clauses derived from Proposition 10, enumerate all optimal solutions in about 30 seconds; the final unsatisfiability, which gives completeness, is certified by a DRAT proof checked by drat-trim and by the verified checker cake_lpr. Section 9 describes the Lean proof, in particular how 191 kernel evaluations were restructured to fit in 2.2 GB of memory, and Section 10.4 lists the running time of every computation.

Outline. Section 2 reviews related work and Section 3 sets up the geometry and the symmetries of the problem. Section 4 proves that every doily of a quadric has degree at least 3. Section 5 proves the main theorem, Section 6 studies the optimal assignments, and Section 7 extends the lower bound to all quadrics. Section 8 discusses the physical consequences, Section 9 the Lean proof, Section 10 the encodings, certificates and running times, and Section 11 open problems.

Related work

Contextuality. The Kochen–Specker theorem [33, 6] and its many proofs are surveyed by Budroni, Cabello, Gühne, Kleinmann and Larsson [10]. Proofs with Pauli observables began with the Peres–Mermin square and Mermin’s pentagram [46, 38, 39]; Waegell and Aravind constructed families of observable-based proofs in the $N$-qubit Pauli group [63], and Trandafir, Lisoněk and Cabello characterised the irreducible magic sets of $n$ qubits [60]. State-independent contextuality was turned into experimentally testable inequalities by Cabello [11, 12] and tested with trapped ions and photons [31, 3]; tests of whole symplectic polar spaces on noisy quantum computers were reported by Holweck [24]. Quantitative measures of contextuality include the contextual fraction of Abramsky, Barbosa and Mansfield [1], in the sheaf-theoretic framework of [2]; the contextuality degree studied here is a combinatorial measure for observable-based proofs, closely tied to the classical value of Mermin-type games [4, 30]. Contextuality is a resource for quantum computation: for magic-state injection [28], for measurement-based computation [48], and for qubit computation models [7].

The finite geometry of Pauli observables. The identification of the $N$-qubit Pauli group modulo phases with the symplectic polar space $W(2N-1,2)$ is due to Saniga and Planat [53], with general qudit versions by Havlicek, Odehnal and Saniga [20] and Thas [58]. This dictionary has been used to classify contextual configurations: Mermin pentagrams as ovoids and their three-qubit taxonomy [51, 36], the Veldkamp spaces of multiple qubits [62], the split Cayley hexagon of order two and its role for three qubits [35, 47, 25], the polar subspaces of small rank [49], and the real four-qubit Pauli group as a hyperbolic quadric of $\mathrm{PG}(7,2)$ with its ovoids [52]. The Lagrangian Grassmannian $\mathrm{LGr}(N,2N)$ relates $N$-qubit and $2^{N-1}$-qubit Pauli groups [27, 34]; for $N=3$ it maps the 135 planes of $\mathrm{W}(5,2)$ to the points of the four-qubit hyperbolic quadric, which is how $\mathrm{DW}(5,2)$ appears in our problem. For the geometry itself we rely on [45, 23, 57, 14].

The contextuality degree. De Boutray, Holweck, Giorgetti, Masson and Saniga [13] introduced the degree and computed it for the quadrics of three qubits (21 and 9). Muller et al. enumerated the multi-qubit doilies and showed that every doily has degree 3 [42]; they then computed degrees of many configurations with SAT solvers and sparse linear algebra, found that the whole three-qubit space $\mathrm{W}(5,2)$ has degree 63, and gave upper bounds for four and five qubits [43]. A heuristic search then gave the upper bounds of Table 1 for four to seven qubits, together with the conjectures that we prove [44]. Saniga et al. explained the value 63 by averaging over doilies and showed that the unsatisfied configurations of $\mathrm{W}(5,2)$ are classically embedded split Cayley hexagons [50, 25]; Muller and Giorgetti identified an abstract structure that determines the degree of observable-based proofs [41], and Muller’s thesis collects the algorithmic side [40]. Our lower bound uses the same averaging principle as [50, 44]; what is new is that, applied to the doilies of a quadric, it is tight, and that its equality case characterises the optimal assignments.

SAT solving and formal proof in mathematics. SAT solvers have settled several long-open combinatorial problems, among them the Boolean Pythagorean triples problem [22], Schur number five [21] and the last open dimension of Keller’s conjecture [9]. Combining SAT solvers with computer algebra (SAT+CAS) was proposed in MathCheck [65]. For Kochen–Specker sets in three dimensions, the minimum size was bounded from below by exhaustive search [61], then by SAT modulo symmetries with co-certificate learning [32] and by SAT+CAS with certified proofs [37]. Unsatisfiability results are made checkable by clausal proofs: DRAT proofs checked by drat-trim [64], and verified checkers such as cake_lpr [56]. Parity constraints such as ours are handled natively by solvers with Gaussian elimination [55]; MaxSAT solvers such as RC2 [29] address the optimisation version directly. Large finite computations have been formally verified before in proof assistants, notably in the proofs of the four colour theorem in Coq [17] and of the Kepler conjecture in HOL Light and Isabelle [19]. Our use of SAT differs from these in that the solver is not used to establish the main theorem: the degree is proved by hand and kernel-checked in Lean [15, 59], and the solver is used only for the classification of the optima, where the encoding is made tractable by lemmas from the proof (§ 10.3).

Pauli observables, quadrics and the contextuality degree

The symplectic polar space

Write $\sigma_{00}=I$, $\sigma_{10}=X$, $\sigma_{01}=Z$, $\sigma_{11}=Y$ for the Pauli matrices. A vector $v=(x\mid z)\in V=\mathbb{F}_2^{2N}$ labels the Hermitian $N$-qubit Pauli observable

and every Pauli observable is $\pm P(v)$ for a unique $v$. For $u,v\in V$ the products satisfy $P(u)P(v)=i^{\varphi(u,v)}P(u+v)$ for an exponent $\varphi(u,v)\in\mathbb{Z}/4$, which is the sum over the qubits of the single-qubit exponents ($XY=iZ$, $YZ=iX$, $ZX=iY$, and $-i$ for the reversed products). Consequently $P(u) and $P(v)$ commute if and only if the symplectic form

vanishes, and they anticommute otherwise. The points of $W(2N-1,2)$ are the nonzero vectors of $V$, that is the $4^N-1$ non-identity observables up to sign, and its lines are the triples $\{u,v,u+v\}$ with $B(u,v)=0$, that is the triples of pairwise commuting observables whose product is $\pm I$.

Quadrics and the real observables

The quadratic forms on $V$ with polar form $B$ are

where $Q_0(v)$ counts the $Y$ factors of $P(v)$ modulo 2. Since $P(v)^{\mathsf T}=(-1)^{Q_0(v)}P(v)$, the singular points of $Q_0$ are exactly the real (symmetric) Pauli observables [52]. The form $Q_0$ is hyperbolic, an orthogonal sum of $N$ hyperbolic planes, and $Q_a(v)=Q_0(v+a)+Q_0(a)$, so $Q_a$ is hyperbolic when $Q_0(a)=0$ and elliptic when $Q_0(a)=1$. For four qubits there are 136 hyperbolic quadrics $Q^+(7,2)$ and 120 elliptic quadrics $Q^-(7,2)$. A hyperbolic quadric of $W(7,2)$ has 135 points and 1575 lines, with 35 lines through each point and 3 points on each line [23]. The lines of a quadric are the lines of $W(7,2)$ all of whose points are singular; two singular points $p\ne q$ are collinear on the quadric if and only if $B(p,q)=0$, since $Q(p+q)=Q(p)+Q(q)+B(p,q)$.

Contexts, signs and the degree

A noncontextual hidden-variable model assigns to each observable a fixed outcome, and quantum mechanics requires the outcomes of $P(u)$, $P(v)$, $P(u+v)$ to multiply to $(-1)^{s(C)}$; so $\deg\mathcal{C}$ is the least number of these constraints that any such model must break. For the configuration $\mathcal{H}_a$ of all points and lines of the quadric $Q_a$ we write $\deg\mathcal{H}_a$.

Two kinds of symmetry leave the degree unchanged.

Proof. Conjugate $P(u)P(v)P(u+v)=(-1)^{s(C)}I$ by $U$.

Every symplectic map of $V$ is induced by a Clifford unitary [18, 16]. For instance, for $r \in V$ the unitary $(I + iP(r))/\sqrt{2}$ induces the symplectic transvection $t_r(v) = v + B(v,r)r$: it fixes $P(v)$ when $B(v,r) = 0$ and sends it to $iP(r)P(v) = \pm P(v + r)$ otherwise. If $Q_0(r) = 0$ then $Q_0(t_rv) = Q_0(v) + B(v,r) = Q_r(v)$, so $t_r$ carries the quadric $Q_r$ onto $Q_0$. Together with Lemma 3, this gives:

Proof. For the hyperbolic quadrics, $t_r$ with $Q_0(r) = 0$ carries $Q_r$ to $Q_0$. For the elliptic ones, $\operatorname{Sp}(8, 2)$ is transitive on the quadratic forms of a given type with polar form $B$ [57]. $\square$

The 136 hyperbolic quadrics fall into three classes by their number of negative lines (532, 604 and 612) [43]; re-signing (Lemma 2) and Clifford transport (Lemma 3) change this number without changing the degree, so it plays no role below.

Grids, doilies and their degree

Proof. Modulo 2, the number of violated contexts is $\sum_{C \in\mathcal{F}}(\sum_{p \in C} x(p) + s(C)) = \sum_C \sum_{p \in C} x(p) + \sum_C s(C) = 0 + 1$. $\square$

A grid is a generalised quadrangle $GQ(2,1)$: nine points $p_{ij}$ ($i,j \in\{1,2,3\}$) and six lines, the three rows $\{p_{i1},p_{i2},p_{i3}\}$ and the three columns $\{p_{1j},p_{2j},p_{3j}\}$. The rows form one ruling and the columns the other.

Proof. Let $r_i$ and $c_j$ be the signs of the rows and the columns, so that the products of the rows and the columns are $(-1)^{r_i} I$ and $(-1)^{c_j} I$. The product $M = P_{11}P_{12}P_{13}P_{21}\cdots P_{33}$ in row-major order equals $(-1)^{r_1+r_2+r_3} I$. Reordering it into column-major order $P_{11}P_{21}P_{31}P_{12}\cdots P_{33}$ exchanges the relative order of $P_{ij}$ and $P_{kl}$ exactly when $i < k$ and $j > l$. There are nine such pairs and each anticommutes, so the column-major product is $(-1)^9M$. It also equals $(-1)^{c_1+c_2+c_3} I$, so $\sum r_i + \sum c_j$ is odd. $\square$

By Lemma 5 (each point lies on one row and one column), every assignment violates an odd number of the six lines of such a grid. This is the familiar argument for the Peres–Mermin square [46, 38]; it also shows that every grid of $W(2N - 1, 2)$ is contextual [26].

A doily of a quadric $Q$ of $W(2N - 1, 2)$ is the configuration of singular points and lines of $Q$ inside a 5-dimensional subspace $U \leq V$ on which $Q$ is nondegenerate. Since $\dim U$ is odd and the characteristic is 2, the restriction of $B$ to $U$ is always degenerate; nondegenerate means that its radical $U \cap U^\perp$ is one-dimensional, spanned by a vector $r$ with $Q(r) = 1$, so that $Q$ is a parabolic form on $U$. It is a parabolic quadric $Q(4,2)$, a generalised quadrangle $GQ(2,2)$ with 15 points and 15 lines [45, 23].

Remark 9. These ten are in fact all the grids of the doily, but only the stated multiplicities are used below. We also checked, on all 40 320 doilies of the four-qubit hyperbolic quadric, that each has exactly ten grids with these multiplicities (Section B).

Proof. Let $x$ be an assignment and $V_D$ the set of violated lines of the doily $D$. Let $G$ run over the ten grids of Lemma 8. By Lemmas 5 to 7, every $G$ meets $V_D$ in an odd number of lines, and by Lemma 8,

The left side is a sum of ten odd numbers, so $4|V_D| \ge10$ and $|V_D| \ge3$. If $|V_D| = 3$, the ten odd numbers sum to 12, so exactly one grid $G^*$ contains three violated lines and the other nine contain one each. Two intersecting violated lines would lie in two common grids (Lemma 8), each then containing at least two, hence three, violated lines; so the three violated lines are pairwise disjoint. They lie in $G^*$, and three pairwise disjoint lines of a grid form a ruling.

The bound is attained: every doily has degree exactly 3 [42 Prop. 1], [13], which we also checked by brute force over the $2^{15}$ assignments of each doily of the four-qubit hyperbolic quadric.

The main theorem

Proof. Lower bound. Let $Q$ be a hyperbolic quadric and $\mathcal{D}$ the set of its doilies. The orthogonal group $O(Q)$ maps doilies to doilies, and it acts transitively on the lines of $Q$ by Witt’s theorem [57], since any linear isometry between two totally singular 2-spaces extends to $V$. The set $\mathcal{D}$ is not empty (an example is given in Section A); so every line lies in the same number $r \ge1$ of doilies, and counting incidences gives $15|\mathcal{D}| = 1575r$. For an assignment $x$ with violated set $\mathcal{V}$, Proposition 10 gives

(In fact $|\mathcal{D}| = 40\,320$ and $r = 384$.)

Upper bound. The assignment of Section A violates exactly 315 of the 1575 lines of the real quadric $Q_0$. Its existence was first shown by Muller et al. [44]; ours was found independently by local search. By Corollary 4, every hyperbolic quadric has an assignment with 315 violations; explicitly, for $Q_0(r)=0$ the assignment $y(v)=x(trv)+\tau(v)$ of Lemma 3 works for $Q_r$, which we also checked for all 135 such $r$.

Remark 12 (The role of the doily). Averaging with grids instead of doilies gives only $|\mathcal{V}| \ge1575/6$, that is $\deg\ge263$, because a grid can have a single violated line out of six. The doily gains from the rounding $\lceil10/4\rceil= 3$. Its violated fraction $3/15 = 1/5$ is exactly the violated fraction $315/1575$ of the quadric, so the lower bound is tight.

Remark 13 (Averaging over three-qubit sections). The quadric $Q_0$ has 120 parabolic hyperplane sections $Q(6,2)$, the sections by $a^\perp$ with $Q_0(a)=1$; each is a copy of $W(5,2)$ with 315 lines, and each line of $Q_0$ lies in 24 of them. If each section, with its inherited signs, has degree 63, which follows from [50] together with [41 Thm. 5], the same averaging gives $\deg\ge120\cdot63/24 = 315$. This route was implicitly available from [44 §5.1.2], which notes the 120 sections, but it was not drawn there. Since the degree 63 of $W(5,2)$ is itself obtained by averaging over doilies [50 §4.1], it is the doily argument in two stages; the direct argument needs only Proposition 10.

The optimal assignments

Equality in the averaging argument constrains every optimal assignment locally.

Proof. If $|\mathcal{V}| = 315$, the inequality $\sum_D |\mathcal{V} \cap D| \ge3|\mathcal{D}|$ is an equality, and each term is at least 3, so each term is 3. Apply Proposition 10. Conversely, if $\mathcal{F}$ covers every line $r'$ times and every doily of $\mathcal{F}$ has three violated lines, then $r'|\mathcal{V}| = 3|\mathcal{F}|$ and $15|\mathcal{F}| = 1575r'$, so $|\mathcal{V}| = 315$.

The converse turns the global optimisation problem over $2^{135}$ assignments into local constraints, each on the fifteen lines of a doily, and this makes a complete enumeration easy.

Proof (computer-assisted). Enumeration. Section 10.2 gives a propositional formula whose models are exactly the optimal assignments (Lemma 19). Enumerating its models with a SAT solver, each new violated set being excluded by a blocking clause, yields 240 violated sets, after which the formula is unsatisfiable; that last unsatisfiability is certified by a DRAT proof checked by drat-trim and, converted to LRAT, by the verified checker cake_lpr [56]. The certificate covers only this unsatisfiability; the correctness of the encoding is Lemma 19, proved by hand (see § 10.2). Gauge. Two assignments have the same violated set if and only if their difference $f$ satisfies $f(u) + f(v) + f(u + v) = 0$ on every line. The line–point incidence matrix has rank 127 over $\mathbb{F}_2$, so these differences form a space of dimension $135 - 127 = 8$, namely the restrictions of the 256 linear functionals on $V$. Consequently, each realisable violated set comes from exactly $2^8 = 256$ assignments. Orbit. The orthogonal group $O^{+}(8,2)$ of $Q_0$ is generated by the 120 transvections $t_r$ with $Q_0(r) = 1$ (reflections), each induced by a Clifford unitary [57]. By Lemma 3 each maps violated sets of optimal assignments to violated sets of optimal assignments. Starting from the violated set of our witness, the orbit under these generators has exactly 240 elements; linear algebra over $\mathbb{F}_2$ confirms that each of them is the violated set of some assignment, independently of the SAT solver, and the orbit coincides with the enumerated list. Since $|O^{+}(8,2)| = 348\,364\,800$, the stabiliser of a violated set has order $1\,451\,520 = |\operatorname{Sp}(6,2)|$, the order of the automorphism group of $DW(5,2)$. Isomorphism. The dual polar space $DW(5,2)$ has as points the 135 planes (maximal totally isotropic subspaces) of $W(5,2)$ and as lines its 315 lines [14]. For each of the 240 violated sets, a backtracking search finds a bijection from the planes of $W(5,2)$ to the points of $Q_0$. We check that, for every line $\ell$ of $W(5,2)$, the three planes containing $\ell$ map to a violated line, and that these images are exactly the 315 violated lines.

Theorem 15 confirms the second half of the conjecture of [44]: the unsatisfiable configurations of the four-qubit hyperbolic quadric are always isomorphic to $DW(5,2)$. Muller et al. explained why one should expect this: $DW(5,2)$ contains 120 split Cayley hexagons of order two, as many as the quadric contains three-qubit subspaces $W(5,2)$, and the unsatisfied configurations of $W(5,2)$ are exactly the classically embedded hexagons [44, 50].

A lower bound for all quadrics

The argument of § 5 uses only the doilies of the quadric and the transitivity of its orthogonal group on lines.

Proof. For a quadric $Q$, a nondegenerate 6-dimensional subspace of type $+$ or $-$ exists for $N\ge3$ (take three of the hyperbolic or elliptic planes of an orthogonal decomposition), and its quadric $Q^{\pm}(5,2)$ contains parabolic sections $Q(4,2)$; so $Q$ has doilies. $O(Q)$ is transitive on the lines of $Q$ by Witt’s theorem, and Proposition 10 applies to every doily. The argument of Theorem 11 gives $|V|\ge3L/15$. For $W(2N-1,2)$, use the doilies of all its quadrics: $\operatorname{Sp}(2N,2)$ permutes them and is transitive on the lines.

For $W(2N-1,2)$ this recovers the bound $(4^{N}-1)(4^{N-1}-1)/15$ of [44 eq. (11)], which was obtained by a recursion over subspaces. The number of lines follows from the fact that the lines of a quadric through a point $p$ correspond to the points of the quadric $p^{\perp}/p$ of rank one less: $L=n_Nn_{N-1}/3$, with $n_N=(2^N-\varepsilon)(2^{N-1}+\varepsilon)$ points on $Q^{\varepsilon}(2N-1,2).$ Table 1 compares the bound with the known exact values and with the heuristic upper bounds of [44].

$N$	configuration	points	lines $L$	$\lceil L/5\rceil$	known value or upper bound
3	$Q^{+}(5,2)$	35	105	21	$=21$ [13]
3	$Q^{-}(5,2)$	27	45	9	$=9$ [13]
3	$W(5,2)$	63	315	63	$=63$ [43, 50]
4	$Q^{+}(7,2)$	135	1 575	315	$=315$ (Theorem 11)
4	$Q^{-}(7,2)$	119	1 071	215	$\le315$ [44]
4	$W(7,2)$	255	5 355	1 071	$\le1 575$ [44]
5	$Q^{+}(9,2)$	527	23 715	4 743	$\le6 975$ [44]
5	$Q^{-}(9,2)$	495	19 635	3 927	$\le7 087$ [44]
6	$Q^{+}(11,2)$	2 079	365 211	73 043	$\le132 391$ [44]
6	$Q^{-}(11,2)$	2 015	332 475	66 495	$\le131 700$ [44]
7	$Q^{+}(13,2)$	8 255	5 720 715	1 144 143	$\le2 331 191$ [44]
7	$Q^{-}(13,2)$	8 127	5 458 635	1 091 727	$\le2 294 580$ [44]

The bound is tight in the four cases where the degree is known. In the other cases the heuristic upper bounds are much larger, between $0.29L$ and $0.42L$. Whether the doily bound is tight for $Q^{+}(9,2)$, as it is for $Q^{+}(5,2)$ and $Q^{+}(7,2)$, is the natural next question.

Physical consequences

A noncontextuality inequality with an exact classical bound. For a configuration with contexts $C=\{u,v,u+v\}$, consider the sum of the signed correlators

where each correlator is estimated by measuring the three commuting observables of $C$ jointly or in sequence [11, 12]. Quantum mechanics gives $\chi=N_C$, the number of contexts, in every state, because $(-1)^{s(C)}P(u)P(v)P(u+v)=I$. A noncontextual model that assigns the outcomes $(-1)^{x(p)}$ satisfies the constraints of the non-violated contexts and violates the others, so $\chi\leq N_C-2\deg C$, and mixtures of such models do no better [30].

The inequality is exact, but it is not stronger than known ones: the ratio of the classical to the quantum value, $945/1575=3/5$, is the same as for the doily ($9/15$), the three-qubit hyperbolic quadric ($63/105$) and the generalised quadrangle $GQ(2,4)=Q^{-}(5,2)$ ($27/45$) [30]. Although $Q^{+}(7,2)$ has 105 times as many contexts as the doily, the two configurations have the same minimum violated fraction, $1/5$. If measurement noise uniformly scales every ideal signed correlator by a visibility $\eta$, the inequality is violated exactly when $\eta>3/5$, as for the doily. Its interest is rather that the classical bound is known exactly for a configuration this large, and that for $Q_0$ all observables are real, so the test needs only real-amplitude (rebit) measurements. By Theorem 17, every quadric of $N\geq3$ qubits violates at least a fifth of its contexts in every noncontextual model, so its ratio is at most $3/5$; the open question is which of them have a violated fraction strictly above $1/5$, that is a ratio strictly below $3/5$. The heuristic upper bounds of [44] for $W(7,2)$, $Q^{-}(7,2)$ and $Q^{+}(9,2)$ are all exactly $5/17$ of their lines, which leaves open a ratio as low as $7/17$.

Where the contextuality sits. Proposition 14 says that in every optimal noncontextual model, the failures are spread perfectly evenly: each doily of the quadric fails on exactly one ruling of one of its grids. Theorem 15 adds that the failures form one rigid geometric object, a $DW(5,2)$, unique up to the symmetry of the quadric. This is the four-qubit analogue of the three-qubit picture of [50], where the unsatisfied lines of $W(5,2)$ always form a classically embedded split Cayley hexagon.

Formal verification in Lean

We formalised the theorem for $Q_0$ in Lean 4 (v4.35.0-rc2) with Mathlib [15, 59]. The toolchain is the release candidate v4.35.0-rc2 because it is the one required by the Mathlib commit we use (045acef0); both are pinned in the repository (lean-toolchain, lake-manifest.json), so lake build fetches exactly these versions, and the build was reproduced from a fresh checkout on a second machine. The final statement is

theorem degree_eq_315 : Contextuality.Pauli.degree 0 = 315

where degree $w$ is the infimum, over all maps $x : \mathbb{N} \to\mathbb{Z}/2$, of the number of violated contexts of the quadratic $Q_w$. #print axioms degree_eq_315 reports only propext, Classical.choice and Quot.sound: the proof uses no sorry, no added axiom, and in particular no native_decide, which would trust the compiler and its runtime.

Definitions. Basic.lean defines points as natural numbers $v < 256$ with the encoding of § 3 (bit $i$ is $x_i$; bit $i+4$ is $z_i$), the symplectic form, the quadratic forms $Q_w$, the phase exponent $\varphi$ as a sum of single-qubit exponents, the contexts as the pairs $(a,b)$ with $a < b < a \oplus b$ satisfying the definition (computed inside Lean by filtering all $256^2$ pairs, so that the list of contexts is not an input), their signs, violation, and the degree. PhaseMatrix.lean proves that $\varphi$ is the exponent in the product of the actual $16 \times16$ Pauli matrices over $\mathbb{C} (pauliMat_mul), so that the sign of every context is the sign of the operator product (context_product`); this ties the combinatorial definition to the physics.

Proof. OddSets.lean proves Lemma 5 (exists_violated_of_odd) for contexts given with point masks. The lower bound follows Theorem 11, with a smaller family than all 40 320 doilies: the 2520 doilies forming the union of the orbits of the qubit permutations $S_4$ on a selected set, which cover every line exactly 24 times (found by integer programming over the orbits). For each doily the data lists its fifteen lines in the order of a fixed labelling of $GQ(2,2)$, so that the ten grids of Lemma 8 sit at the same fifteen positions in every doily. The kernel then checks: (i) the keys of $2520 \cdot15 = 37\,800$ listed lines form a permutation of the 1575 contexts, each repeated 24 times (keys_perm); (ii) in every doily, each of the ten grids is an odd set: the exclusive-or of the point masks of its six lines is 0 and their signs sum to 1; (iii) each of the fifteen positions lies in four grids (sum_gridPos). Together with Lemma 5 this gives three_le_doily and $24|V| \ge3 \cdot2520$, hence le_numViolated: $315 \le|V|$ for every assignment. A kernel evaluation of the witness (witness_check) gives the upper bound. Nothing produced by the scripts that generate the data is trusted: every property of the data used in the proof is re-evaluated by the kernel, and the data’s sortedness is never assumed.

Making the kernel computation fit on a laptop. All finite checks are discharged by decide +kernel, which evaluates a decidable proposition in the kernel. The kernel caches intermediate terms, so its memory grows with the number of reduction steps. Three naive checks did not fit: evaluating contexts 0 (a filter over $256^2$ pairs) in one check exceeded a 4 GB limit, and a single sort-and-compare of all 37 800 keys was estimated, from the measured growth, at about 10 GB. We restructured the proof so that no check is large:

• Q8PlusContexts.lean states the contexts as 64 literal chunks and proves contexts_eq : contexts 0 = (List.range 64).flatMap cchunk by 64 separate kernel checks; every later check rewrites with it instead of recomputing the filter.

• The permutation check (i) is split twice: for each of 26 chunks of 100 doilies, a merge sort of its 1500 keys equals a literal bucketed by key/1024 (sortOK); for each of the 64 buckets, the merged pieces from the 26 chunks equal the corresponding chunk of contexts, each repeated 24 times (bucketOK). The merge functions are proved to permute their input (mergeTree_perm) and a lemma on exchanging two flatMaps up to permutation (flatMap_comm_perm) glues the chunks, so the correctness of the sorting is never assumed.

• Each Lean file imports only the Mathlib modules it needs: importing all of Mathlib alone costs about 4 GB of memory.

The development has 191 decide +kernel checks. Table 2 lists its files.

File	lines	build	content
Basic.lean	133	10 s	definitions; degree
OddSets.lean	144	34 s	Lemma 5; merge sort and its permutation lemmas
PhaseMatrix.lean	86	27 s	phase rule for the Pauli matrices over $\mathbb{C}$
Q8Plus.lean	240	16 s	the proof of degree_eq_315
Q8PlusData.lean (generated)	6 266	55 s	2520 doilies, grid positions, witness
Q8PlusContexts.lean (generated)	580	71 s	contexts in 64 chunks; 67 kernel checks
Q8PlusChecks.lean (generated)	226	276 s	120 kernel checks: cover, sorting, grids

The formalisation covers the real quadric $Q_0$. The other 135 hyperbolic quadrics follow from Corollary 4, which we checked by computer but did not formalise. The Lean proof does not formalise the general arguments of § 4: instead of Lemmas 7 and 8, the kernel checks the grid structure and the odd-set property directly on each of the 2520 doilies it uses. Likewise Theorem 17 for other quadrics and other $N$ is not formalised. Theorem 15 is not formalised; its certificate is the DRAT proof of § 10.2, checked by drat-trim and by cake_lpr.

Computations: encodings, certificates and costs

This section is written for readers who want to check or reuse the computations. All of them are in the repository; Table 4 lists their running times.

Computation	tool	time
all finite facts of the paper (verify_facts.py)	Python	47 s
with the degree 3 of all 40 320 doilies by brute force over $2^{15}$ assignments	Python, NumPy	55 s
separately written re-check of the bound and the witness (independent_check.py)	Python, NumPy	72 s
search for a witness (find_witness.py)	Python	under 1 s
enumeration of the 240 optimal violated sets (enumerate_optimal.py)	CaDiCaL 1.5.3	30 s
of which the final refutation		2 s
DRAT proof of the final refutation (39 MB)	CaDiCaL 3.0.1	25 s
DRAT check	drat-trim	11–17 s
LRAT check of the converted proof	cake_lpr	3 s
orbit, realisability, 240 isomorphisms with $DW(5,2)$ (optimal_structure.py)	Python	4 s
table of lower bounds for all quadrics (general_bounds.py)	Python	0.1 s
all $2^{28}$ quadratic assignments	C	2.4 s
Lean build of degree_eq_315 (Mathlib precompiled)	Lean 4	under 10 min
axiom report	Lean 4	15 s

What is computed, and who checks it

• Finite facts used in the proofs (numbers of quadrics, points, lines and signs; the doilies, their grids and multiplicities; the witness): computed by one Python program, recomputed by a second one written separately, and, for $Q_0$, re-evaluated by the Lean kernel. The signs are computed both from the phase rule and from $16 \times16$ matrix products.

• Theorem 11: the lower bound is a proof by hand (§ 4 and § 5); the upper bound is the evaluation of the witness on 1575 lines. Both are kernel-checked in Lean for $Q_0$.

• Theorem 15: the completeness of the list of 240 violated sets rests on the SAT encoding of § 10.2 and on a DRAT proof checked by drat-trim and, as LRAT, by the verified checker cake_lpr. The orbit, the realisability of each set and the isomorphisms with $DW(5, 2)$ are checked by separate code that does not use the SAT solver.

• Remark on quadratic assignments: an exhaustive search in C.

The SAT encoding of the optimal assignments

The degree problem is an instance of MAX-XOR-SAT: 135 Boolean variables and 1575 parity constraints of length three, one per line, and the task is to satisfy as many as possible. Rather than optimise, we use Proposition 14 to characterise the optimum by local constraints.

• Variables. $x_p$ for the 135 points and $v_C$ for the 1575 lines.

• Parity. For each line $C = \{a,b,c\}$, the eight clauses that forbid the assignments of $(v_C,x_a,x_b,x_c)$ with $v_C + x_a + x_b + x_c \ne s(C)$, so that $v_C$ holds iff $x$ violates $C$ (12 600 clauses).

• Local cardinality. For each doily $D$ of a family $\mathcal{F}$ covering every line equally often, “exactly three of the fifteen $v_C$, $C \in D$, are true”, encoded by PySAT’s CardEnc.equals with its sequential-counter encoding [54], which combines an “at most 3” and an “at least 3” counter (144 clauses and 72 auxiliary variables per doily; these are PySAT’s sizes, smaller than those of the textbook encoding). We use either the 2520 doilies of the Lean proof or all 40 320.

• Pair clauses (redundant). For any two intersecting lines $C,C'$ of a common doily, the clause $\neg v_C \lor\neg v_{C'}$. There are 37 800 such pairs: through each point, two of its 35 lines lie in a common doily iff they are not coplanar on the quadric. These clauses are not derived by the solver: they are justified by Proposition 10, applied to every doily of the quadric (not only to those of $\mathcal{F}$), and they are part of the input formula whose unsatisfiability the certificate checks.

• Blocking clauses. After a model with violated set $\mathcal{V}$, the clause $\bigvee_{C\in\mathcal{V}}\neg v_C$. Since every model has $|\mathcal{V}| = 315$, it excludes exactly the models with violated set $\mathcal{V}$.

Proof. By Proposition 14 (converse), every model is optimal. Conversely, an optimal assignment has exactly three violated lines in every doily, which are pairwise disjoint by Proposition 10, so it satisfies all cardinality and pair clauses with the auxiliary variables of the sequential counters set accordingly.

No symmetry breaking is used: the gauge freedom of § 6 leaves 256 models per violated set, and the blocking clauses act on the $v$-variables only. The final formula, the base formula plus the 240 blocking clauses, has 183 150 variables and 413 520 clauses in the default configuration. CaDiCaL 3.0.1 [8] refutes it and writes a DRAT proof of 39 MB; drat-trim [64] verifies it, using 120 460 of the 560 025 lemmas in the run recorded in the repository (CaDiCaL’s proof differs slightly between machines; the formula itself is fixed by its SHA-256 hash in drat/check.log). The proof was also converted to LRAT by drat-trim (22 MB) and checked by the verified checker cake_lpr [56], whose correctness is proved in HOL4 down to machine code. The certificate establishes only that the final formula is unsatisfiable. Three parts of the argument are trusted rather than certified: the encoder, a short Python program that writes the formula; Lemma 19, including the justification of the pair clauses by Proposition 10; and the enumeration loop, whose only role is to add one blocking clause per violated set it finds, all of which appear in the certified final formula.

What made the enumeration easy

Muller et al. [43, 44] attacked the degree with SAT solvers and with heuristics directly, and the direct formulations remain hard. Table 3 compares, with the same solver and a time limit of 30 minutes, two direct formulations with the four variants of our encoding. The direct formulations are a MaxSAT instance (the parity clauses as hard clauses, $\neg v_C$ as 1575 soft clauses, solved by RC2 [29]) and the decision problem “at most 314 violated lines” with a totalizer encoding [5], whose unsatisfiability is the lower bound of Theorem 11.

Formulation	variables	clauses	result within 30 min
MaxSAT (RC2)	1 710	12 600 + 1 575 soft	not solved
SAT, at most 314 violated (totalizer)	18 562	1 268 978	not solved
local cardinality, 2520 doilies	183 150	375 480	all 240 by 44 s; not refuted
local cardinality, 40 320 doilies	2 904 750	5 818 680	all 240 by 1363 s; refuted at 1447 s
local cardinality, 2520 doilies + pairs	183 150	413 280	all 240 by 29 s; refuted at 31 s
local cardinality, 40 320 doilies + pairs	2 904 750	5 856 480	all 240 by 403 s; refuted at 407 s

Three observations stand out. First, neither direct formulation finishes: RC2 does not reach the optimum and the solver does not refute “at most 314” within 30 minutes, although Theorem 11 shows that the answer is 315. The lower bound is therefore not merely faster to prove by hand; for these generic encodings it is out of reach of the solver in this time. Second, the local cardinality constraints make the search easy: every variant finds all 240 optimal violated sets. Third, completeness, the refutation after the last blocking clause, depends on the redundant pair clauses: without them the small family is not refuted within 30 minutes and the large one needs 84 s for the last call alone; with them the final call takes 2 s and 4 s. The pair clauses encode the second half of Proposition 10, that the violated lines of a doily are pairwise disjoint, so they are a lemma of the proof handed to the solver. The smaller family is also better: the 2520 doilies of the Lean proof give a formula 14 times smaller than all 40 320, and the full enumeration takes 31 s instead of 407 s.

Running times

All times in Table 4 are wall-clock times on a laptop (Apple M3, 8 cores, 16 GB, macOS 14.5), with one thread and at low priority while other programs were running, so they are upper bounds on what a dedicated machine needs. Software: Python 3.12.12 with NumPy 2.5.4 and PySAT 1.9 (which bundles CaDiCaL 1.5.3); the standalone CaDiCaL 3.0.1; drat-trim at commit 2e3b2dc; cake_lpr at commit a36874a; Lean 4 v4.35.0-rc2 with Mathlib at commit 045acef0.

Open problems

1. The elliptic quadric and the whole space. For four qubits, $215 \le\deg Q^{-}(7,2) \le315$ and $1071 \le\deg W(7,2) \le1575$ from Theorem 17 and [44]. Every line of $W(7,2)$ lies on 24 of the 120 elliptic quadrics, so $\deg Q^{-}(7,2) = 315$ would give $\deg W(7,2) \ge120 \cdot315/24 = 1575$ and hence equality. The doily bound cannot reach 315 here, and neither can averaging over the 136 parabolic sections $Q(6,2)$ of $Q^{-}(7,2)$, which also gives only $\lceil136 \cdot63/40 \rceil= 215$; larger sub-configurations are needed.

2. Five qubits. Is $\deg Q^{+}(9,2) = 4743$? The heuristic upper bound 6975 of [44] is far above.

3. A conceptual proof of Theorem 15. Proposition 14 characterises the optimal violated sets by local conditions on doilies. Is there a direct proof that these conditions force a $DW(5,2)$, for instance through the Lagrangian Grassmannian map from the planes of $W(5,2)$ to the points of $Q^{+}(7,2)$ [27, 44]?

4. Higher rank. Does a hyperbolic quadric $Q^{+}(2N-1,2)$ have degree $L/5$ whenever 5 divides $L$, and are its optimal violated sets again a single orbit?

Code and data availability

All scripts, the witness, the SAT certificates and the Lean development are at https://github.com/BrianLi009/four-qubit-hyperbolic-quadric; Section B lists what each checks.

The witness and an example doily

The following assignment of $Q_0$ violates exactly 315 of its 1575 lines. It gives the value 1 (outcome $-1$) to the 71 observables below and 0 (outcome $+1$) to the other 64 real four-qubit observables.

IIIX IIIZ IIXX IIXZ IIZX IIZZ IXIX IXIZ IXXZ IXZX IXZZ IYIY
IYYI IYYX IYZY IZII IZIZ IZXI IZYY IZZZ XIII XIIX XIXX XIYY
XIZI XXII XXXI XXXX XXYY XXZI XYXY XYYZ XZII XZXI XZXZ XZZI
XZZX YIIY YIXY YIYI YIYZ YXIY YXXY YXYI YXZY YYII YYXI YYZI
YZYX YZZY ZIIX ZIIZ ZIXX ZIXZ ZIZX ZXIX ZXIZ ZXXX ZXXZ ZXYY
ZXZX ZXZZ ZYIY ZYXY ZYYI ZYZY ZZII ZZXI ZZYY ZZZI ZZZZ

The 315 violated lines pass through every point, seven through each, and form a $DW(5,2)$ (Theorem 15).

An example of a doily of $Q_0$: the singular points of the subspace spanned by XIII, IXII, ZIII, IZIX and YIYI. Its fifteen points are XIII, IXII, XXII, ZIII, ZXII, IZIX, XZIX, ZZIX, YYIX, YIYI, YXYI, IYYX, XYYX, YZYX, ZYYX, and three of its fifteen lines are negative: {XXII, ZZIX, YYIX}, {ZXII, XYYX, YZYX} and {XZIX, YXYI, ZYYX}.

Reproducing the computations

From the folder code of the repository, with Python and the packages numpy and python-sat:

command	reproduces
python verify_facts.py --brute	every finite fact of Sections 3 to 5; the witness
python independent_check.py	the same, separately written
python enumerate_optimal.py --cnf	Theorem 15: the 240 sets and the final formula
sh drat/check.sh	the DRAT proof, its check, and the LRAT check by cake_lpr (needs CaDiCaL and drat-trim; cake_lpr if present)
python optimal_structure.py	Theorem 15: orbit, realisability, isomorphisms with $DW(5, 2)$
sh sat_ablation.sh, sh sat_direct.sh	Table 3
python general_bounds.py	Table 1
sh quadratic/run.sh	the remark on quadratic assignments

In the folder lean, run lake exe cache get to download the compiled Mathlib, then lake build, and finally lake env lean scripts/AxiomReport.lean for the axiom report. Every script exits with a non-zero status if a check fails.