Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorOperatorSpace

Abstract

LatticeSectorOperatorSpace

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.

Definition 1.1 (Coefficients).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.Coefficients

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.Coefficients (✓ 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.

Coefficients on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Definition 1.2 (leftTerm).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.leftTerm

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.leftTerm (✓ 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.

leftTerm on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Definition 1.3 (firstTerm).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.firstTerm

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.firstTerm (✓ 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.

firstTerm on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Definition 1.4 (secondTerm).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.secondTerm

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.secondTerm (✓ 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.

secondTerm on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Definition 1.5 (Lawful).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.Lawful

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.Lawful (✓ 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.

Lawful on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Theorem 1.6 (canonical_lawful).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.canonical_lawful

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.canonical_lawful (✓ 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.

The actual restricted mixed field satisfies statewise truncation, both derivative laws and full three-term Borcherds with all three finite supports. These are derived from accepted ordinary Y.

Definition 1.7 (operatorSpace).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.operatorSpace

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.operatorSpace (✓ 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.

operatorSpace on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Definition 1.8 (IO).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.IO

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.IO (✓ 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.

IO on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Definition 1.9 (canonicalIO).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.canonicalIO

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.canonicalIO (✓ 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.

canonicalIO on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Theorem 1.10 (ward).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.ward

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorOperatorSpace.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.

ward 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.

References