发表机构
Yanbiao Lab, DataCanvas Co., Ltd.; Peking University（研标实验室，数据立方有限公司; 北京大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出秩递减稀疏迹树原群，自动生成并验证28个新的五阶奥斯汀定律的不限基数反模型，并发出Lean 4证书。
AI 中文摘要
有限模型查找器无法见证奥斯汀定律：一个恒等式，其有限模型都是平凡的，但存在非平凡的不限基数模型。我们引入了秩递减的稀疏迹树原群，这是在可数无限构造子树载体上的有限表示的全运算。默认乘积将其参数配对；有限多个正Horn子句定义了例外情况。我们的主要过程从符号求值迹中推导子句。对于找到的每个模型，它通过构造子大小的降阶证明例外关系的功能性，通过穷举符号情况分析证明恒等式，并发出自包含的Lean 4证书。最小同步不动点给出了与实现无关的语义，因此有界搜索可能错过模型，但不会使已认证的结果失效。在ETP的96个五阶奥斯汀候选中，我们发现了28个恒等式的不限基数反模型，并通过Lean验证，这些恒等式在我们审计中先前没有公开分类。它们形成14个对偶类，并确立了28个新的奥斯汀分类。四个ALPS已知案例使总数达到32个已认证候选。在Canonical-4187上，即Order5-130和4,141行ALPS池的去重并集，一次新的迹运行产生636个证书，全部被Judge v3接受。在相同的资源限制下，Vampire 5.0.1、E 3.5.1和完整的Twee 2.6.1共同证明了94个规范类中的蕴含关系。只有Twee返回可信的反可满足结果，涉及18个类；独立的有限侧证书强制其中16个为不限基数的。这些ATP中没有一个发出显式模型或Lean证书，也没有一个判定28个新分类。据我们审计所知，这是第一个自动合成此迹树模型族、生成良基逆推证明并发出自包含Lean 4证书的系统。
英文摘要
Finite model finders cannot witness an Austin law: an identity whose finite models are all trivial but which has a nontrivial infinite model. We introduce rank-decreasing sparse trace-tree magmas, finitely presented total operations on a countably infinite constructor-tree carrier. The default product pairs its arguments; finitely many positive Horn clauses define exceptions. Our main procedure derives clauses from symbolic evaluation traces. For every model found, it proves functionality of the exceptional relation by descent on constructor size, proves the identity by exhaustive symbolic case analysis, and emits a self-contained Lean 4 certificate. A least simultaneous fixed point gives an implementation-independent semantics, so bounded search may miss models but cannot invalidate certified results. On ETP's 96 order-five Austin candidates, we discover and Lean-verify infinite countermodels for 28 identities with no prior public classification in our audit. They form 14 duality classes and establish 28 new Austin classifications. Four ALPS-known cases bring the total to 32 certified candidates. On Canonical-4187, the deduplicated union of Order5-130 and the 4,141-row ALPS pool, a fresh trace run produces 636 certificates, all accepted by Judge v3. At equal resource limits, Vampire 5.0.1, E 3.5.1, and complete Twee 2.6.1 jointly prove implications in 94 canonical classes. Only Twee returns trusted counter-satisfiable outcomes, for 18 classes; independent finite-side certificates force 16 to be infinite. None of these ATPs emits an explicit model or Lean certificate, and none decides the 28 new classifications. To the best of our audit, this is the first automated system to synthesize this trace-tree model family, generate well-founded inversion proofs, and emit self-contained Lean 4 certificates.
Comments34 pages, 2 figures, 7 tables. Code and reproducibility artifacts: https://github.com/YanbiaoLab/trace-tree-magmas
