完成仿射顶点代数极大理想的Arakawa--Moreau猜想的Lean 4验证报告
A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras
浏览论文内容
中文总结 AI 辅助
本报告用Lean 4形式化验证了Arakawa--Moreau猜想的仿射顶点代数极大理想新证明，涵盖关键演绎与案例，声明为论文局部推理的内核检查而非完整表示论重构。
中文摘要 AI 辅助
我们报告了一项Lean 4形式化审计，该审计伴随论文“完成仿射顶点代数极大理想的Arakawa--Moreau猜想”（arXiv:2607.25249）。在单个Lean源文件中，开发内核检查了用于新极大理想情形的论文局部演绎架构：仿射核检测与提升、极值PBW线演绎、有限Ramond--Casimir算术与情形枚举、简化单纯性矛盾方案，以及-1级D_l族和D4、E6、E7、E8正参数情形的案例级仿射结论。它还审计了论文中替代的D_l -2级论证以及第8节中单独的降秩应用。先前已发表的例外n=0情形不被声称为此包的新形式化结果。发布的项目在固定的Lean/Mathlib环境下成功构建，并包含对主要最终包装器的实时#print axioms查询。\n 该开发并未从Mathlib中的基础定义重构仿射顶点代数、最小W-代数、BRST/DS约化、Ramond Zhu理论或Li谱流。这些成分，连同案例特定表示论对象的具体实现，被暴露为定理参数和语义接口。因此，精确的验证声明是从明确陈述的VOA/BRST/DS边界输入对论文局部证明的内核检查演绎，而非对周围表示论的从头形式化。
英文摘要
We report a Lean 4 formal audit accompanying the paper "Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras" (arXiv:2607.25249). In a single Lean source, the development kernel-checks the paper-local deductive architecture used for the new maximal-ideal cases: affine-kernel detection and lifting, extremal PBW-line deductions, finite Ramond--Casimir arithmetic and case enumerations, reduced-simplicity contradiction schemes, and the case-level affine conclusions for the level -1 D_l family and the positive-parameter cases of D4, E6, E7, and E8. It also audits the paper's alternative D_l level -2 argument and the separate rank-reduction application of Section 8. Previously published exceptional n=0 cases are not claimed as newly formalized results of this bundle. The released project builds successfully with the pinned Lean/Mathlib environment and contains live #print axioms queries for the principal final wrappers. The development does not reconstruct affine vertex algebras, minimal W-algebras, BRST/DS reduction, Ramond Zhu theory, or Li spectral flow from foundational definitions in Mathlib. Those ingredients, together with the concrete realization of case-specific representation-theoretic objects, are exposed as theorem parameters and semantic interfaces. Accordingly, the precise verification claim is a kernel-checked deduction of the paper-local proof from explicitly stated VOA/BRST/DS boundary inputs, rather than a from-scratch formalization of the ambient representation theory.
发表机构
- Sichuan University（四川大学）
机构由 AI 辅助整理，请以论文原文为准。
