A Lean 4 Verification Report for Subregular Affine Cells and the Level $-1$ Vertex Algebra of Type $D$

Sihai Jin

math.QA Aug 21, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

Lean 4 kernel-checks internal deductions of the subregular affine cell classification for the level -1 type-D vertex algebra from explicit representation-theoretic interfaces.

Abstract

We report a Lean 4 formal verification accompanying the paper "Subregular Affine Cells and the Level -1 Vertex Algebra of Type D" (arXiv:2608.11997). The formalization kernel-checks substantial internal parts of the proof architecture, including the Section 4 membership/descent chain, the type-D norm-gap argument, zero-orbit energy and signed-permutation rigidity, node-weight and numerical rigidity calculations, the exhaustion logic, the passage to the candidate quotient classification, the simple-object count, the final additive Grothendieck-group comparison, and the coefficient-substitution layer of the uniform character formula. Higher representation-theoretic results whose foundational infrastructure is not presently constructed in the file are isolated as explicit semantic interfaces rather than introduced as Lean axioms. Thus the precise claim is a kernel-checked internal deduction from explicit representation-theoretic boundary inputs, not a from-scratch formalization of vertex algebras, BRST reduction, finite W-algebras, or affine Hecke theory inside Mathlib.

Problem

The Shan–Yan–Zhao affine left-cell conjecture for the level -1 vertex algebra L_{-1}(D_ℓ), ℓ≥5, classifies simple objects in the vacuum block and identifies the Grothendieck group with a specialized dual affine cell module. Verifying such a representation-theoretic proof requires distinguishing kernel-checked deductions from foundational infrastructure not present in Mathlib.

Approach

A single Lean 4 file separates the proof into internally kernel-checked calculations and external representation-theoretic facts exposed as structured semantic interfaces rather than axioms. Higher results (twisted vertex algebras, BRST reduction, finite W-algebras) are represented via typed parameters and hypotheses. Lean assembles membership/descent chains, type-D norm-gap and rigidity arguments, exhaustion logic, quotient classification, and the additive Grothendieck-group isomorphism from these inputs.

Results

The top-level theorem DTypeMainTheorem.theorem_1_1 derives the classification predicate, an equivalence giving ℓ+1 simple objects, and an additive-group isomorphism. The 10,511-line source has 304 declarations, no sorry/admit, no user-declared axioms, and #print axioms reports only [propext, Classical.choice, Quot.sound].

Paper result	Lean declaration	Boundary
Lemma 4.5	lemma_4_5_vacuum_central_zero	scalar cancellation kernel-checked
Theorem 4.10	theorem_4_10_membership	ideal containment derived
Theorem 5.14	theorem_5_14_from_propositions_5_5_and_5_13	orbit branches assembled in Lean
Theorem 6.1	theorem_6_1	descent/exhaustion internal

Selected paper-to-Lean verification map entries

Papers With

A Lean 4 Verification Report for Subregular Affine Cells and the Level $-1$ Vertex Algebra of Type $D$