A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.27952
curl -X POST /api/v1/records/arxiv/2609.27952/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.27952/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'