The best known lower bound for the minimum Kochen-Specker vector system in $\mathbb{R}^3$ -- 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.
Comments
Lean 4 and Python sources, certificates, and CI at https://github.com/shayaansiddique06/kscert
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.
Companion paper to "Exact rigidity certificates for Kochen-Specker sets, the graded flex dictionary, and the Peres-Penrose circle" (https://doi.org/10.5281/zenodo.21488473). A complete algebraic theory of Kernaghan's two-symbol alphabet landscape (arXiv:2603.16988). Results: (1) the exhaustive 80-case d=3 classification: exactly FOUR independent cancellation mechanisms (rational, modulus-2, phase, golden), not two - a fifth candidate is proved identical to the phase mechanism under the alphabet's own x<->1/x gauge duality - and any generator avoiding all four provably yields a 3-colorable pool (structure theorem via Godsil-Zaks); (2) the d=4 extension: a term-alphabet lemma, 16 new mechanisms from the 280-case 4-term classification, and no colorable regime (Peres-24 anchors every pool); (3) the mechanism-moduli audit across the census, proving the forward flex bound in general; (4) the uniqueness theorem: a machine-certified KS-coloring of the full 145-ray M3-line-stable graph proves the Gould-Aravind circle is the unique positive-dimensional flexible family of two-symbol d=3 KS sets - including the honest retraction of a tempting arithmetic explanation that failed direct verification; (5) the M2 mirror: the maximal circle-stable graph is KS-uncolorable, compactness pins the M2 circle to exactly five integer-trace exact points, and the Gaussian points x=+-(1+i) carry a NEW 49-ray KS core (SAT-certified with a three-anchor-validated encoder, critical, and exactly rigid) distinct from all six census islands and from the survey's own Gaussian island (shown here to reduce to Peres-33). Flexibility tracks the circle's four conjugation-fixed points exactly (Hypothesis L), and a J-splitting construction makes the real/skew flex decomposition well-posed at conjugation-symmetric non-real points. Every claim carries an explicit evidence label (PROVED / EXACT / NUMERICAL / CONJECTURE / OPEN), each backed by a script in the attached verification suite (also public: https://github.com/manuflog/contextuality-obstructions/tree/main/rigidity). Methods note: large-language-model assistants (Anthropic Claude) were used substantially in drafting and in developing the verification suite; every mathematical claim is machine-verified independently of that assistance, and the author takes full responsibility for the results. Version 4 (July 2026) — status of the Observation 28/29 point. This paper extends and in one place corrects Part II of Kernaghan's survey (arXiv:2603.16988). The specific disputed point, the reported non-persistence of the Peres/Penrose flex, was conceded by its author in v8 of that preprint, in a labelled correction note that also publishes the cause. References are updated to v8 and the passage now describes the matter as settled. As elsewhere in this series, v8 is not treated as independent confirmation of finiteness: its continuation is double precision and its modular rank computation bounds flex only from above, as its author states. Version 5 (July 2026) — a proof step is withdrawn and replaced. The theorem is unchanged. Versions up to v4 justified the last step of the structure theorem (necessity of a mechanism for the raw pool) by invoking Godsil–Zaks, paraphrased as “rational-coordinate projective ray sets in R^n are always 3-colorable”, and concluded that the x=3 graph is 3-colorable. Both halves are false and are withdrawn. The paraphrase is false: the x=2 raw pool is a rational-coordinate ray set (49 rays, 138 orthogonal pairs) with chromatic number 4. The application is false at the pool it was applied to: the x=3 graph is not 3-colorable either, also chromatic number 4. Godsil–Zaks concerns rational points of the unit sphere, and a rational ray such as (1,1,1) does not normalize to one, so the theorem never applied to these pools at all. The theorem itself is unaffected. Graph 3-colorability was only ever a sufficient route to KS-colorability, and KS-colorability at x=3 is established directly by exhaustive certificate — 31488 distinct valid KS colorings, recomputed independently for this version. Both chromatic numbers were verified twice, by DSATUR backtracking and by SAT (Glucose3). An earlier section of the paper had already retracted this same invocation for the Re(x) = -1/2 line; that retraction should have been applied to the structure theorem at the same time and was not. It is now. Also corrected: earlier versions described cross-product completion as “the closure step that rescues the Golden and CK-31 islands from initial colorability”. That is wrong for CK-31, whose raw pool at x=2 is already KS-uncolorable (49 rays, 138 pairs, 26 triads, no valid coloring). Completion enlarges it but is not needed for uncolorability. Only the Golden island is genuinely rescued by completion. Version 6 (July 2026) — a theorem is scoped, its closed-pool reading withdrawn, and the resolution identified. The structure theorem (“no mechanism, no KS set”) was stated through v5 without an alphabet hypothesis. For Hermitian-closed complex pools it is FALSE, and the cause is a term the classification missed: with x* as an entry, (x*)*·x = x² appears, so the closed term set is {±1, ±x, ±x*, ±N, ±x², ±(x*)²}. Counterexample, verified twice in independent exact implementations: x = √3 + i avoids every locus M1–M5, yet its closed pool (145 rays / 390 pairs / 30 triads) is KS-uncolorable; unclosed it is colorable. The identity x² + (x*)² = N holds along the whole lines arg x ≡ ±30° (mod 180°), at every modulus — a positive-dimensional uncolorable locus outside the classification. The resolution, also in this version: the new lines carry no new mechanism at core level and no new flexible family. Along them the ratio x/x* is a primitive sixth root of unity at every modulus, and projective rescaling identifies the lines’ uncolorable content with the known Eisenstein island: the line-stable graph is constant in the modulus away from a finite exceptional set, all 23 of its minimal uncolorable cores (complete enumeration) consist of modulus-independent rays, every core has mechanism flex exactly 0, and all 43 rays of the certified core embed projectively into the closed ω-pool. The pool’s one genuine deformation (flex exactly 1) lives entirely on colorable decoration rays. The uniqueness theorem — the Gould–Aravind circle as the unique positive-dimensional flexible family, scoped to M1–M4 — is unaffected. A complete x²-extended classification of closed-pool identities is recorded as open. The theorem is restated with the unclosed-alphabet hypothesis (under which it is true, and true for all real x); the term-alphabet lemma, correct as literally stated, now carries its scope explicitly. Found by the program’s own adversarial verification gate; every number above is from exact arithmetic with SAT and backtracking engines agreeing. Version 7 (July 2026) — the open problem left by v6 is closed, and the two-mechanism dichotomy is restored. v6 corrected a scope error (with x* as an entry the product x² appears, so the published 80-case classification is incomplete for Hermitian-closed pools) and recorded the complete x²-extended classification as open. This version carries it out. The classification. The closed term set has six types, giving 224 three-term cases; 126 are impossible for every nonzero x, and the rest reduce to the published loci M1–M5 together with exactly four new positive-dimensional loci — x²+(x*)² = ±N (the lines arg x = ±30° and ±60°) and x²+(x*)² = ±1 (two rectangular hyperbolae) — plus eight isolated points, all of which lie on the 60° line. Restricted to the 80 published cases the same computation returns exactly the 54 impossible cases and exactly M1–M5, reproducing the original theorem. The corrected dichotomy, now a theorem rather than an open problem. The closed raw pool is KS-uncolorable if and only if (A) |x|² ∈ {2, 1/2} or x ∈ {±2, ±1/2}, or (B′) x/x* is a primitive third or sixth root of unity. Established by an audit of all 58 realizable locus-membership classes, using the fact that the index-labelled closed graph depends only on which loci x belongs to. Why this is deflationary, and the point of the version. A ratio lemma explains the new uncolorable loci rather than adding a mechanism: projective rescaling by 1/x* carries the degree-one sub-pool isomorphically onto the pool over {0, ±1, ±r} with r = x/x*, multiplying every inner product by 1/N and so preserving orthogonality exactly. Since |r| = 1, the uncolorable cases are precisely those where r is a primitive third or sixth root of unity, and there the sub-pool is the unclosed Eisenstein pool at every modulus. The two hyperbola loci are genuinely new identities but carry no uncolorable content at any point tested; the arg = 45° locus, where r = i has order four and the pool is colorable, shows that being a root of unity is necessary but not sufficient. Consequence for the two-mechanism reading. Hermitian closure does not break the dichotomy reported in arXiv:2603.16988; it relocates one half of it. The literal rule “|x|² ≥ 3 and x not a root of unity implies colorable” fails — x = √3 + i is a counterexample — but that x has x/x* = e^{iπ/3}, and the corrected statement is again exactly two mechanisms: modulus, acting on x; phase, acting on x/x*. We read this as identifying the correct invariant for the phase mechanism rather than as a counterexample to the pattern. Verification scripts x2class_derive.py, x2class_pools.py, x2class_scan.py, x2class_deflate.py and x2class_closure.py accompany this version in the public repository; every colorability verdict was decided by SAT and by an independent backtracker in agreement, in exact arithmetic in the appropriate number field.
We construct Lean-kernel-checked spectral certificates for rational definite pencils representing the periodic SU(2) Kogut–Susskind ladder with link spins truncated at `j ≤ 1`. The construction uses an unnormalised spin-network basis with a positive diagonal Gram matrix. At unit coupling and circumferences `N = 3, 4`, the certificates enclose both centre-sector ground energies and give strict lower bounds for both sector first-excited energies. They identify a simple charge-0 ground level and a simple charge-1 first-excited level of the full pencil, with full spectral gaps in `[0.865089, 0.865122]` and `[1.183111, 1.183144]`, respectively. The gap therefore increases strictly between these two sizes. Compared with the independently certified `j ≤ ½` gaps at the same sizes and coupling, it decreases strictly at both sizes, while the first excitation remains in the nontrivial centre sector. The `N = 4` sector dimensions are 579 and 434. Their certificates use separately kernel-checked arithmetic segments composed by proved chain lemmas, with measured segment-process memory near 1.6 GiB; the final aggregation has a larger memory requirement. The final theorems use only `propext`, `Classical.choice` and `Quot.sound`. The spectral certificates are kernel-checked statements about the supplied pencils. Their interpretation as statements about the truncated Hamiltonian is established by a hybrid verification: kernel-checked finite identities, paper proofs of the spin-network identification, and independent exact-rational verification of the selection-eligible magnetic contractions, with vanishing elsewhere established by the selection-rule proof and stored-support certificates. The full identification chain is not kernel-checked. No cutoff-convergence or untruncated-gap conclusion is asserted. This bundle contains the manuscript draft, the 57445-module Lean 4 acceptance closure (acceptance command `lake build ChristMath.J1Accept`), the exact pencils and local tables, the emitters, the independent Rust implementation, and the fresh-process axiom audit.
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.
Computing the distance of a stabilizer code is NP-hard, yet certifying the distance of a given code needs no search at all — only two one-sided certificates that meet. An upper bound is a single explicit logical operator: one vector, checked in milliseconds against the actual check matrix — it commutes with every stabilizer, it is provably outside their span, and it acts on exactly w qubits. A lower bound is a universal statement — no logical operator lives below weight w — discharged by a finite scan whose completeness is itself a theorem, not a convention: a reconstruction lemma proves that every light Pauli vector appears in the scanned list, so the scan quantifies over the whole space rather than over a table someone chose. When the two certificates touch, the distance is exact, and the receipt can be replayed by a referee who trusts neither the authors nor their software. We build this bracket calculus over the binary symplectic carrier, close it exactly on the classical menagerie — the five-qubit perfect code, Steane, Shor, the distance-three rotated surface code, and the 3 × 3 toric code — and report an instructive refutation: our own frozen reference data claimed distance at least 2 for a punctured code fragment, and the certificate layer produced an explicit weight-one logical operator. Puncturing buys a logical qubit and leaves it bare; the count and the distance are independent shadows of the same subgroup lattice. The same prover-proposes/kernel-disposes architecture certifies logical counts at bivariate-bicycle scale (k = 12 at n = 144) from change-of-basis rank certificates checked in linear time, and every number in the system wears a two-valued trust badge whose semantics is an event, not a citation: no kernel run on your instance, no badge. The results are proved in a machine-checked formal kernel. Published by The Institute for Applied Ontological Mathematics.
Within the program of identifying rigid Kochen-Specker (KS) sets (Xu-Saha-Bharti-Cabello, PRL 132, 140201; Trandafir-Cabello, PRA 111, 052204; Kernaghan, arXiv:2603.16988), this paper contributes exact-arithmetic certificates, one unification, and one correction. The two flexible islands of Kernaghan's landscape (Peres-33 and Z[sqrt(-2)]-33) are the two antipodes of a single exact circle of complex 33-ray KS sets, the closed form of the Gould-Aravind phase family. We certify flex=1 exactly at both islands, prove local completeness, and correct Kernaghan's Observation 28: the flex is finite, not merely infinitesimal. The circle contains no degenerations (proved exactly) and its Sum P = 11 I mechanism is resolved via hyperoctahedral orbit tight frames. Exact rigidity certificates across the full known census make Peres-Penrose-33 the unique flexible KS set. The Hermitian rigidity matrix block-diagonalizes at real points (flex_C = flex_R + flex_skew) with the graded cycle split proved, and a torsion layer is proved flex-invariant. Every claim carries an explicit evidence label (PROVED / EXACT / NUMERICAL / LITERATURE / OPEN). The attached verification suite (35+ self-checking scripts) reproduces every certificate; companion hardware notebooks (IBM Quantum, two devices) confirm the witness-invariance prediction Sum P = 11 to 0.45% and measure the loop holonomy eigenphase to ~2%, consistent with the exact value 2*pi*sqrt(1867)/33. Note on methods: large-language-model assistants (Anthropic Claude) were used substantially (drafting, verification-script development, literature search, proof proposals); all mathematical claims are machine-verified by the attached suite, and the author takes full responsibility. Code and data: https://github.com/manuflog/contextuality-obstructions
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.