LatticeSectorReconstruction
Abstract
LatticeSectorReconstruction
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 (ground_current_ward).
Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorReconstruction.ground_current_ward
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorReconstruction.ground_current_ward (✓ 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.
ground_current_ward on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.
Theorem 1.2 (ground_sequence_detects_zero).
Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorReconstruction.ground_sequence_detects_zero
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorReconstruction.ground_sequence_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.
ground_sequence_detects_zero on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.
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.