Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorBorcherds

Abstract

LatticeSectorBorcherds

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

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.action

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

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

Definition 1.2 (sectorT).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.sectorT

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

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

Theorem 1.3 (single_canonical).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.single_canonical

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

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

Theorem 1.4 (single_action).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.single_action

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

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

Theorem 1.5 (single_sectorT).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.single_sectorT

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

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

Theorem 1.6 (canonical_truncation).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.canonical_truncation

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

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

Theorem 1.7 (canonical_source_derivative).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.canonical_source_derivative

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

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

Theorem 1.8 (canonical_target_derivative).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.canonical_target_derivative

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

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

Definition 1.9 (mixedLeft).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.mixedLeft

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

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

Definition 1.10 (mixedFirst).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.mixedFirst

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

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

Definition 1.11 (mixedSecond).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.mixedSecond

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

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

Theorem 1.12 (canonical_borcherds).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorBorcherds.canonical_borcherds

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

canonical_borcherds 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