Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeSectorFullFusion

Abstract

LatticeSectorFullFusion

The actual neutral Heisenberg category has arbitrary finite lists of integral charges, with repeats and arbitrary finite-dimensional complex multiplicities. Morphisms commute with every actual neutral mode. No finite global charge set is fixed. Construction covers degenerate forms and rank zero; the universal classification assumes both inverse Gram equations over complex matrices.

Definition 1.1 (FullCoefficients).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.FullCoefficients

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

FullCoefficients is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.2 (coordinate).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.coordinate

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

coordinate is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.3 (fullLeft).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullLeft

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

fullLeft is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.4 (fullFirst).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullFirst

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

fullFirst is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.5 (fullSecond).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullSecond

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

fullSecond is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.6 (FullLawful).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.FullLawful

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

FullLawful is the actual mixed-sector construction or law stated by its compiled telescope.

Theorem 1.7 (fullLawful_iff).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullLawful_iff

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

Complete full-carrier truncation, both derivatives, and supported three-term Jacobi are equivalent to the component laws; both directions are proved.

Definition 1.8 (fullOperatorSpace).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullOperatorSpace

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

fullOperatorSpace is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.9 (FullIO).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.FullIO

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

FullIO is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.10 (fullIOEquiv).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullIOEquiv

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

fullIOEquiv is the actual mixed-sector construction or law stated by its compiled telescope.

Theorem 1.11 (fullIO_lawful).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullIO_lawful

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

fullIO_lawful is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.12 (fullUniversal).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullUniversal

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

Complete lawful mixed fields are represented by actual Hom from the sum-charge sector. The explicit inverse is componentwise normalized ground evaluation on matching charges and zero on every wrong charge.

Theorem 1.13 (fullUniversal_apply).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullUniversal_apply

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

fullUniversal_apply is the actual mixed-sector construction or law stated by its compiled telescope.

Definition 1.14 (fullPost).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullPost

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

fullPost is the actual mixed-sector construction or law stated by its compiled telescope.

Theorem 1.15 (fullPost_apply).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullPost_apply

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

At every source state u, target-source state v and integer coefficient n, fullPost D H hHG hGH α β g acts by the actual target module map g.val on I.val u n v.

Identity coherence (fullPost_identity): for every D : LatticeData, H : Matrix (Fin D.rank) (Fin D.rank) ℂ, hHG : H * gramComplex D = 1, hGH : gramComplex D * H = 1, α β : Charge D, M : FiniteSectorObject D and I : FullIO D α β M, one has fullPost D H hHG hGH α β (identity D M) I = I.

Composition coherence (fullPost_comp): for the same D, H, hHG, hGH and α β, every M N P : FiniteSectorObject D, g : Hom D M N, h : Hom D N P and I : FullIO D α β M satisfy fullPost D H hHG hGH α β (compose D h g) I = fullPost D H hHG hGH α β h (fullPost D H hHG hGH α β g I).

These are repo-derived consequences of fullPost_apply. Subtype extensionality, linear-map extensionality and function extensionality in n reduce the equations to coefficients. The pointwise formula reduces the identity law to I.val u n v = I.val u n v and the composition law to h.val (g.val (I.val u n v)) = h.val (g.val (I.val u n v)), by the definitions of identity and compose.

The objects and Hom operations are those of the actual finite-sector neutral Heisenberg category, and FullIO is the complete mixed-target IO subspace. No finite global charge set is fixed; repeated charges, arbitrary finite multiplicities and rank zero remain in scope. The two inverse-Gram hypotheses are retained for both laws.

Theorem 1.16 (fullUniversal_natural).

Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorFullFusion.fullUniversal_natural

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

fullUniversal_natural is the actual mixed-sector construction or law stated by its compiled telescope.

This is classical free-boson and lattice mathematics: Bakalov-Kac math/0402315v1 section 4.1 and Matsuo-Nagatomo reconstruction. Imported residue/Pascal and Sugawara suppliers retain Scott Carnahan and Kalle Kytola attribution. Tensor products encode multiplicities only. No literature novelty, full charged lattice-module fusion, coherent braiding or associativity, pentagon/hexagon, Monster anomaly, string theory or CFT realization is claimed.

References