Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorHom

Abstract

LatticeSectorHom

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

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.sectorHomSpace

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

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

Definition 1.2 (SectorHom).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.SectorHom

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

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

Definition 1.3 (scalarHom).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.scalarHom

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

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

Theorem 1.4 (hom_translation).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.hom_translation

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

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

Definition 1.5 (postCoefficients).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.postCoefficients

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

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

Theorem 1.6 (post_lawful).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.post_lawful

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

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

Definition 1.7 (post).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.post

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

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

Theorem 1.8 (hom_scalar).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.hom_scalar

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.hom_scalar (✓ 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_scalar on the actual charge-labelled oscillator sectors; the precise parameters and conclusion are the compiled Lean statement.

Theorem 1.9 (hom_wrong_charge).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorHom.hom_wrong_charge

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