{"id":"d789d24f-18b0-43cc-906d-c9c1ae92d953","arxiv_id":"2607.26413","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"Exact rational case-tree certificates, replayed by a sound Lean checker, prove non-embeddability in R³ for all 180 distinct graphs in the published blocking database.","lead":"This paper introduces machine-checked proof certificates that verify, through a formally verified Lean checker, that 180 graphs from the published Kochen-Specker lower-bound pipeline cannot be embedded in R³. It closes a trust gap in the geometric half of the best-known 24-vector bound and exposes reproducibility issues in the original pipeline.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The Lean kernel proof is sound for the embedded graphs, but the parser bridging the published blocking files to those embedded graphs is unverified; a misparse would make the certificates prove non-embeddability of the wrong graphs.","rationale":"The reader's weakest_assumption identifies the same load-bearing concern: the mapping from the published geometric-half pipeline to the formal `Cert` objects relies on faithful transcription of external artifacts. I agree. The machine-checked part of the argument is unusually strong: `check_sound` is a Lean kernel theorem under a minimal axiom closure, and the per-graph theorems are closed kernel theorems. I considered other potential objections—the use of `by decide` for a statement about real vector assignments, the possibility that fuel exhaustion could reject valid certificates, and the unsoundness of a leaf type—but none of these undercuts the central claim: fuel can only cause refusal, never acceptance, and the soundness theorem is machine-checked against the actual checker implementation. The one place where trust must cross an unformalized boundary is the extraction of graph edge lists from the published PhysicsCheck and Uijlen-Westerbaan artifacts. That boundary is not covered by `check_sound`, and the paper's own findings demonstrate that the artifacts are error-prone. However, the paper has taken reasonable provenance measures: SHA-256 pins, Python replay, explicit colex edge lists, and adversarial mutation tests. This makes the concern testable rather than a demonstrated flaw. For a preprint with moderate confidence and an available artifact, the appropriate verdict remains ACCEPT, with the concrete parser-conformance test as the condition that would settle the residual risk.","tokens_in":10322,"tokens_out":17435,"duration_ms":151288,"concrete_test":"Independently re-implement the parser in a different language (e.g., Rust or OCaml) for the SHA-256-pinned PhysicsCheck blocking files and the Uijlen-Westerbaan order-13 list, and compare the resulting 291 line-level edge lists (180 distinct) and the 44-candidate classification against the colex edge lists embedded in the Lean theorem declarations and the JSON certificates in the repository. Run this on the exact pinned commits, including the order-12 file with no trailing newline, and verify that every edge list matches. If any edge list differs, the certificates prove non-embeddability of a different graph; if all match, the provenance bridge is sound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central formal claim is `check_sound`: if the Lean checker accepts a `Cert`, there is no realization of that certificate's graph. This is kernel-checked and not the weak point. The weak point is the provenance of the `Cert` objects: they are claimed to be transcriptions of 291 source lines from PhysicsCheck's order-10/11/12 blocking files and seven order-13 Uijlen-Westerbaan graphs. The only bridge from the published artifacts to the embedded edge lists is a Python replay script and SHA-256 pins. That bridge is outside the machine-checked theorem. The paper's own Findings 4 and 5 show the published files are subtle—missing trailing newline, 155 distinct versus 266 lines, unreproducible 41/44 candidate counts—so a parser bug, e.g., off-by-one in line splitting, mishandling a file without a trailing newline, misinterpreting vertex numbering, or applying the wrong subgraph-containment semantics, would silently change the graph being certified. Then the closed kernel theorems would be correct but for the wrong graphs, and the claim that the geometric half of the published bound is closed would not transfer. This is an artifact-trust concern, not an internal inconsistency.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces exact rational case-tree certificates for real non-embeddability of orthogonality graphs, and claims to certify all 291 source lines (180 distinct graphs) of the published PhysicsCheck blocking lists plus seven order-13 Uijlen–Westerbaan minimal graphs. The certificates are replayed by a pure-Python checker and by a total checker implemented in Lean 4, with a kernel-checked soundness theorem whose axiom closure is {propext, Classical.choice, Quot.sound}. Each per-graph non-embeddability result is claimed to be a closed kernel theorem proved by `decide`. The paper also reports findings about the published pipeline, including a load-bearing injectivity condition, hidden WLOG case obligations, and an unreproducible final-candidate count.","tokens_in":10576,"tokens_out":7546,"duration_ms":67685,"significance":"If the claims hold, this is a substantial contribution. It replaces an uncheckable Z3 nonlinear-real-arithmetic component of a flagship computational bound with exact, replayable certificates, and it does so with a machine-checked soundness theorem, a minimal and mechanically enforced axiom closure, kernel-reducible verdicts, and adversarial validation. The explicit treatment of unresolved obligations and the detailed audit of the published pipeline are also strengths. The main residual risk is the unformalized bridge from the published artifact files to the edge lists embedded in the certificates; this is an artifact-trust concern rather than an internal inconsistency, but it is load-bearing for the paper's central claim that the geometric half of the published bound is closed for the blocking database.","major_comments":[{"comment":"The central external claim — that the 291 source lines of the published blocking database are faithfully represented by the certificate edge lists — is not machine-checked. The only bridge is a Python replay script and SHA-256 pins, both outside the Lean kernel. The paper itself demonstrates that line counts and filter semantics are delicate (missing trailing newline, 155 vs 266 distinct lines, 41 vs 43 candidate counts). A parser or line-splitting error would make the closed kernel theorems correct but for the wrong graphs, so the claim that the geometric half of the published bound is closed would not transfer. Please provide the parsed edge lists for all 180 graphs as a standalone machine-readable artifact with an independent audit path, or formalize the parsing/provenance layer, and state the trust boundary explicitly in the abstract and introduction.","section":"§5.1, Findings 4 and 5; §4.2"},{"comment":"The statement that 42 of the 44 final order-22/23 candidates are discharged by seven order-13 certificates depends on the external 933-graph Uijlen–Westerbaan list and on a replication of the published filter whose semantics are not machine-checked. The paper's resolution of the 41/43 discrepancy is based on pinned artifacts, not on a Lean-verified classification. This is load-bearing for the claim that the order-13 row \"does real work for the full bound.\" Please separate the machine-checked part (seven order-13 graphs are certified non-embeddable) from the external classification and containment analysis, or supply verified containment witnesses for the 42 candidates.","section":"§5.1, Finding 5"}],"minor_comments":[{"comment":"Please clarify the arithmetic relating \"exactly 42 of the 44 contain one of seven order-13 UW minimal graphs\" to Finding 5's statement that \"exactly 41 contain an order-13 UW minimal graph\" among the 43 order-23 survivors. The order-22 survivor must be accounted for explicitly.","section":"§5.1"},{"comment":"In the `positiv` leaf, state explicitly that p_1,...,p_m are the residual pool polynomials of the current branch; the current text leaves this implicit.","section":"§3.3, Eq. (1)"},{"comment":"The displayed theorem `c10_0_nonembeddable` refers to \"graph #0\" without showing the edge list. Either include the explicit colex edge list in the statement or provide a pointer to the pinned transcription so the reader can see what graph is being certified.","section":"§4.2"},{"comment":"The row \"order-12 shard 20\" should clarify what a \"shard\" is and why only 20 certificates appear there while Table 2 lists 155 distinct order-12 graphs. The relationship between shards, source lines, and distinct graphs is not immediately clear.","section":"Table 3"},{"comment":"Consider stating explicitly that \"closed for blocking DB\" in the T5 row means the Z3 verdicts for the blocking database are replaced by certificates, not that the full T5 layer for all order-22/23 candidates is closed. Section 7 already scopes this, but Table 1 could be read too strongly.","section":"§2.2, Table 1"}],"recommendation":"major_revision","confidential_remarks":"This is a strong paper with a machine-checked core, and the internal formalization appears sound. My main concern is the trust boundary between the published artifacts and the certificate edge lists: it is not machine-checked, yet it is load-bearing for the paper's central claim. I would not reject, but the authors should tighten the provenance story — for example, by publishing the parsed edge lists for all 180 graphs and providing a more rigorous independent audit, or by explicitly narrowing the claim to the transcribed graphs. I did not find internal mathematical errors in the certificate design or the soundness argument."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this paper does the real work it claims. It replaces an uncheckable Z3 trust link in the geometric half of the Kochen–Specker lower bound with exact rational certificates, replayed by two independent checkers, and it proves soundness in Lean with per-graph verdicts as closed kernel theorems. It also surfaces genuine discrepancies in the published pipeline — injectivity as a load-bearing condition, a hidden WLOG branch, and an unreproducible candidate count. Those findings alone make it worth a close read.\n\nThe most solid part is the architecture. The certificate format is precise: WLOG anchoring, propagation schedules, factorization/SOS splits, and leaves discharged by injectivity, ideal membership, or a Positivstellensatz-style positivity argument. Every check is exact rational arithmetic. The soundness theorem covers all eight node kinds, and the non-embeddability results are stated as closed Lean theorems proved by decide. As far as I can tell from the PDF, the formal core holds up.\n\nThe soft spot is exactly where the stress-test note points: the bridge from the published blocking files to the graph objects the certificates live on. The certificates prove non-embeddability for embedded edge lists; the claim that these are the graphs from the published pipeline depends on a Python replay script and SHA-256 pins, not on a machine-checked theorem. The paper's own Findings 4 and 5 show the published files are subtle — missing trailing newline, 155 distinct versus 266 lines, 41 vs 43 candidates — so a parser bug would silently change the certified graph. That is a genuine artifact-trust gap. It could be closed by making the parser/serialization formally verified, or at least by providing a precise, machine-checked correspondence between source files and certificate graphs. This doesn't undermine the internal soundness of the Lean proofs, but it does constrain what you can conclude about the published bound.\n\nI could not run the repository from the PDF. The claims about kernel reducibility and the 115-mutation adversarial suite are asserted from the repo, not demonstrated in the text. The two unresolved final candidates are handled honestly as explicit obligations, and the absence of an end-to-end ≥24 theorem is stated plainly. These are limitations, not red flags.\n\nWho this is for: anyone working on verified computational proofs, and anyone who wants to know whether the geometric half of the KS bound is actually checked. It deserves a serious referee, with particular attention to the artifact and the parser bridge.","headline":"Genuinely useful formal-verification work that closes the uncheckable Z3 gap on the KS blocking database; the main residual risk is the unverified parser bridge from published files to certified graphs.","tokens_in":11048,"tokens_out":2080,"would_cite":true,"duration_ms":18950,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68V20","14P10","05C62"],"pacs":[],"model":"deepseek-v4-flash","headline":"Machine-checked certificates now close the geometric half of the 24-vector Kochen-Specker lower bound.","keywords":["Kochen-Specker theorem","vector systems","non-embeddability certificates","exact rational arithmetic","sum-of-squares proofs","machine-checked proofs","proof assistants","graph realizability"],"falsifier":"Independently search for a realization of any graph that the checker accepts: if any nonzero, pairwise ray-distinct vectors in R^3 satisfy all edge orthogonalities, the soundness theorem would be inconsistent. A simpler first test is to feed the checker a known-embeddable graph and require rejection, and to rerun the published filter on the pinned hashes to check the reported 43/44 candidate count.","tokens_in":10190,"feed_emoji":"📐","tokens_out":4551,"duration_ms":39665,"temperature":0.7,"pith_summary":"This paper claims to close the main trust gap in the best known lower bound for the minimum Kochen-Specker vector system: the part that showed candidate graphs cannot be embedded in R^3. The published proof relied on a nonlinear real arithmetic solver that returned answers without checkable evidence. The paper introduces exact rational case-tree certificates, each encoding a WLOG normalization, a propagation schedule, and a finite case analysis whose leaf proofs are polynomial factorizations and rational sum-of-squares identities. Two checkers, one standalone and one inside a machine-checked proof assistant, replay the certificates with no shared code, and the soundness theorem behind the proof-assistant checker is kernel-verified. The paper argues that acceptance by that checker implies no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph, so every one of the 291 source lines (180 distinct graphs) in the pipeline's blocking lists now has a closed machine-checked non-embeddability theorem.","feed_headline":"Exact certificates close the geometric half of the KS bound","feed_subtitle":"All 180 blocking graphs now carry machine-checked non-embeddability proofs, no solver trust required.","key_machinery":"The central object is the rational case-tree certificate: a self-contained document recording an anchor, a propagation schedule, a parameter list, and a finite case tree. The tree's nodes split on polynomial factorizations (over an integral domain, a product zero forces a factor zero) and rational sum-of-squares identities (over a formally real field, a sum of squares zero forces each term zero); leaves close branches by injectivity collisions, ideal membership with explicit cofactors, or a Positivstellensatz-shaped positivity identity involving products of pair-injectivity polynomials. The work it does is to reduce real non-embeddability to identities checked by exact rational arithmetic, s","core_discovery":"The central claim is that for every graph in the published blocking database, non-embeddability in R^3 can be witnessed by a finite, exact-rational object whose correctness is independently decidable. Each certificate anchors a triad or edge to basis vectors, replays a schedule of cross-product and plane-parametrization steps that expresses all vertex vectors as polynomials in a few parameters, and presents a case tree. Internal splits are factorization or sum-of-squares identities checked by expansion; leaves are discharged by injectivity collisions, obligation collapse, ideal membership with explicit cofactors, or a Positivstellensatz-shaped positivity argument. Because the checker is prov","pith_inferences":["A natural next step beyond this paper is to produce direct certificates for the two remaining final candidates, since the verified chain currently carries them as explicit hypotheses rather than closed theorems.","The certificate format's reliance on explicit propagation schedules suggests it could generalize to other finite-dimensional geometric realizability questions, provided those questions admit a similarly rigid WLOG normalization.","The documented gap between the published count of 41 and the recomputed 43 final candidates implies that future reproductions of the bound must fix a canonical filter semantics before comparing candidate counts.","If the checker's soundness theorem is robust, the same certificate-and-replay architecture could be reused to certify non-embeddability in other orthogonality-graph problems, not just Kochen-Specker systems."],"forward_implications":["If correct, the geometric half of the lower-bound proof no longer depends on trusting a nonlinear real arithmetic solver; every blocking graph's non-embeddability is independently replayable and kernel-checked.","The seven order-13 certificates discharge 42 of the 44 final candidates through verified subgraph monotonicity, so the path to a fully verified bound of at least 24 is reduced to two unresolved candidates plus the remaining layers of encoding correctness, canonicity, and streaming SAT proof replay.","The same certificate format should transfer to other real-algebraic non-embeddability problems where the obstruction is real-geometric rather than purely algebraic, since leaves can speak about positivity and injectivity loci.","The findings about the published pipeline show that building proof objects can surface discrepancies, such as an unreproducible candidate count and hidden case obligations, that are invisible to solver-trusting workflows."],"fun_headline_variants":["Every KS blocking graph now has a Lean 4 proof","Exact rational certificates banish solver trust from KS bound","Machine-checked non-embeddability for all 180 graphs","Z3-free: exact case-tree proofs for every blocking graph","Formal proofs close the geometric half of KS lower bound"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The whole chain transfers to the published Kochen-Specker bound only if the 291 source lines and the filter semantics from the original pipeline were transcribed exactly; if the parse, pinning, or candidate replication is wrong, the certificates prove non-embeddability of graphs other than the pipeline's actual candidates.","fun_headline_variants_meta":{"raw":{"variants":["Every KS blocking graph now has a Lean 4 proof","Exact rational certificates banish solver trust from KS bound","Machine-checked non-embeddability for all 180 graphs","Z3-free: exact case-tree proofs for every blocking graph","Formal proofs close the geometric half of KS lower bound"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000247,"raw_usage":{"total_tokens":1437,"prompt_tokens":857,"completion_tokens":580,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":601,"completion_tokens_details":{"reasoning_tokens":506}},"tokens_in":601,"tokens_out":580,"duration_ms":5383,"temperature":1.0,"reasoning_tokens":506,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T16:29:31.714530+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Independently search for a realization of any graph that the checker accepts: if any nonzero, pairwise ray-distinct vectors in R^3 satisfy all edge orthogonalities, the soundness theorem would be inconsistent. A simpler first test is to feed the checker a known-embeddable graph and require rejection, and to rerun the published filter on the pinned hashes to check the reported 43/44 candidate count.","supporting_citations":[],"review_version":1}