v1.0.0 — Initial Lean verification release

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.