AI 中文总结
该研究针对最小科亨-斯佩克界几何半部分的不可嵌入性，提出机器可验证的精确有理情形树证书，在Lean 4中实现验证器，解决了原证明的不可验证问题并修正了流水线缺陷。
AI 中文摘要
R³中最小科亨-斯佩克向量系统的已知最佳下界为24个向量，该下界基于一个计算证明，其组合半部分可生成DRAT证明，但几何半部分不行：数千个候选图的不可嵌入性由Z3的非线性实算术确定，该工具无法生成可验证的证明对象。我们针对该证明的阻塞数据库填补了这一空白，引入了实不可嵌入性的精确有理情形树证书，其拆分形式为多项式因式分解和有理平方和分解，叶节点由单射性、理想成员关系或正合性形式的正性论证验证，我们验证了已发布流水线中从10阶到13阶阻塞列表的全部291条源行（180个不同图）。证书由两个与生成器无代码共享的独立验证器重放：一个基于精确分数的纯Python重放器，以及一个在Lean 4中实现并验证了正确性的完整验证器。正确性定理（接受意味着不存在满足射线单射性、正交性要求的非零实向量分配来实现该图）通过公理闭包{propext, this http URL, this http URL}进行内核验证，且无最大公约数的有理算术层使整个判定计算可内核归约，因此每个图的不可嵌入性结果都是通过decide证明的封闭内核定理。形式化过程还发现了已发布流水线的相关问题，包括其可嵌入性概念中承载负载的单射性侧条件、基于Z3的工作流不可见的隐藏WLOG情形义务，以及我们针对已发布人工制品解决的不可复现候选数量问题。所有证书、验证器和证明均可从单个构建中获取并重放。
英文摘要
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.
CommentsLean 4 and Python sources, certificates, and CI at https://github.com/shayaansiddique06/kscert
