A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras
Abstract
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.
Related
- Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras
- A Computational Verification of the Markov Uniqueness Conjecture for z≤ 10500000
- The_Quadratic_Conjecture_and_p-groups_of_maximal_class
- Discriminants of Hermitian forms, maximal degenerations and Kontsevich's tropical approach to the Hodge conjecture
- On a conjecture on the Kasami APN function: reductions, structure theorems, a proof for kbmod n∈{1,2,n−2,n−1}, and exhaustive verification for n≤ 13
BibTeX
@misc{jin2026lean,
title = {{A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras}},
author = {Sihai Jin},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.27952},
eprint = {2609.27952},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.27952},
}
RIS
TY - UNPB
TI - A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras
AU - Sihai Jin
PY - 2026
DA - 2026/09/01
PB - arXiv
DO - 10.48550/arxiv.2609.27952
UR - https://arxiv.org/abs/2609.27952
AB - 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.
ER -