LatticeSectorClassification
Abstract
LatticeSectorClassification
Construction uses arbitrary ordinary symmetric even integral lattice data, including degenerate forms, zero charges and rank zero. Classification and universality require an explicit two-sided complex inverse Gram matrix, with no positivity or integer unimodularity.
Theorem 1.1 (conformal_translation).
Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorClassification.conformal_translation
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorClassification.conformal_translation (✓ std3). ∎
Citation. Atsushi Matsuo; Kiyokazu Nagatomo (1997). On axioms for a vertex algebra and the locality of quantum fields. URL: https://arxiv.org/abs/hep-th/9706118v1.
Commentary.
conformal_translation on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.
Theorem 1.2 (normalized_ground_detects_zero).
Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorClassification.normalized_ground_detects_zero
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorClassification.normalized_ground_detects_zero (✓ std3). ∎
Citation. Atsushi Matsuo; Kiyokazu Nagatomo (1997). On axioms for a vertex algebra and the locality of quantum fields. URL: https://arxiv.org/abs/hep-th/9706118v1.
Commentary.
A zero normalized ground coefficient forces the whole lawful IO to vanish. Downward induction from statewise truncation uses positive-current Ward, the actual current commutant, and conformal L0. The two oscillator recurrences then reconstruct both full inputs.
Classical sources are Bakalov-Kac, arXiv math/0402315v1, section 4.1, and Matsuo-Nagatomo free-boson reconstruction. Imported residue/Pascal and Sugawara suppliers retain Scott Carnahan and Kalle Kytola source attribution and licenses. No literature novelty is claimed.
The category is the neutral Heisenberg sector category. Full charged lattice-VOA modules, dual-lattice coset fusion, coherent associativity and braiding, pentagon and hexagon, Monster or twisted anomaly, CFT, string theory and AdS/CFT remain additional unproved edges. Rank zero has one charge and a one-dimensional IO space; it is not the zero theory.