Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorCategory

Abstract

LatticeSectorCategory

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 (FiniteSectorObject).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.FiniteSectorObject

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

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

Definition 1.2 (States).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.States

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

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

Definition 1.3 (mode).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.mode

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

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

Definition 1.4 (translation).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.translation

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.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.

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

Definition 1.5 (homSpace).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.homSpace

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

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

Definition 1.6 (Hom).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.Hom

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

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

Definition 1.7 (identity).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.identity

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

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

Definition 1.8 (compose).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.compose

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

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

Definition 1.9 (incomingSpace).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.incomingSpace

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

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

Definition 1.10 (Incoming).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.Incoming

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

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

Definition 1.11 (incomingEquiv).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.incomingEquiv

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

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

Definition 1.12 (Intertwiners).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.Intertwiners

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

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

Definition 1.13 (universal).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.universal

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

Postcomposition with the actual canonical intertwiner gives a complex linear equivalence from actual neutral-module maps into an arbitrary finite charge sum to its component IO space.

Definition 1.14 (coefficients).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.coefficients

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.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.

Theorem 1.15 (universal_coefficients).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.universal_coefficients

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

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

Definition 1.16 (withMultiplicities).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.withMultiplicities

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

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

Definition 1.17 (multiplicityCoordinates).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.multiplicityCoordinates

Formalization. D5/S3/VertexAlgebra/Sectors/LatticeSectorCategory.multiplicityCoordinates (✓ 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 basis of each arbitrary finite-dimensional complex multiplicity space identifies its tensor multiplicity carrier with repeated charge coordinates. The tensor products here encode multiplicities, not the representing fusion object.

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