Initial public release of the Lean 4 verification accompanying
Sihai Jin, "Subregular Affine Cells and the Level -1 Vertex Algebra of Type D".
This release contains:
SubregularAffineCells.lean- the frozen Lean/Mathlib environment;
- reproducibility information;
- Section 4, 5, and 6 formalization-boundary audits.
Verified environment:
- Lean 4.34.0-rc1
- Mathlib v4.34.0-rc1
- compilation exit code: 0
- final theorem:
DTypeMainTheorem.theorem_1_1 - axiom audit:
[propext, Classical.choice, Quot.sound]
This release is intended to correspond to the initial arXiv version of the verification report.