Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual Theta-Fixed Rootless Low Grades

Abstract

Production lattice reflection and the literal canonical Sugawara fixed low-energy spaces.

Definition 1.1 (Free negation orbits).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.NormFourOrbit

Formalization. D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.NormFourOrbit (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

The quotient identifies a norm-four integral charge with its negative. Integral torsion-freeness and the norm equation exclude fixed charges; a constructed equivalence with orbit times Bool proves that the natural shell cardinality is twice the orbit cardinality.

Definition 1.2 (Orbit representative).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.normFourOrbitRep

Formalization. D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.normFourOrbitRep (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

A classical representative is used to write each basis vector. No orientation, enumeration or norm-four count is assumed.

Definition 1.3 (Actual energy-two configuration coordinates).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.TwoConfig

Formalization. D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.TwoConfig (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

For positive definite rootless even LatticeData, the all-charge low-grade basis identifies the literal energy-two labels with a mode-two oscillator, an unordered pair of mode-one colours including repetition, or a norm-four charged ground state.

Definition 1.4 (Fixed energy-two basis indices).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.FixedTwoIndex

Formalization. D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.FixedTwoIndex (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

The indices are the unordered neutral pairs and the free norm-four negation orbits. Empty rank and empty shells remain in scope.

Definition 1.5 (Signed coordinate permutation).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.coordinateTheta

Formalization. D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.coordinateTheta (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

This linear endomorphism negates the mode-two neutral coordinates, fixes the neutral pair coordinates and exchanges the two charge coordinates in every negation orbit. Its relation to production theta is proved rather than assumed.

Definition 1.6 (Complete actual grade-two coordinates).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.gradeTwoCoordinateEquiv

Formalization. D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.gradeTwoCoordinateEquiv (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

For positive definite rootless even LatticeData, gradeTwoBasis gives a linear equivalence from the complete actual grade to the configuration function space. Positivity proves shell finiteness; there is no charge cutoff or replacement carrier.

Theorem 1.7 (Production theta conjugacy on the full actual grade).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.theta_gradeTwo_coordinate_transport

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.theta_gradeTwo_coordinate_transport (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

For every positive definite rootless even LatticeData D and every vector in its actual energy-two grade, production LatticeInvolution.theta is the inverse coordinate equivalence applied to coordinateTheta of that vector’s coordinates. The proof checks production theta_single and sigma_monomial on all three basis sectors, then uses basis extensionality.

Definition 1.8 (Basis of the literal canonical fixed L0 eigenspace).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.actualFixedEnergyTwoBasis

Formalization. D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.actualFixedEnergyTwoBasis (✓ std3).

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

For positive definite rootless even LatticeData, a basis indexed by neutral unordered pairs and norm-four negation orbits is constructed for fixedSpace D intersected with the eigenspace at two of sugawaraMode D (gramComplex D) inverse zero. The coordinate conjugacy identifies the actual intersection with the invariant coordinate space. ActualL0_eigenspace_eq_grade supplies the exact Sugawara bridge. Each neutral basis vector in the actual canonical fixed eigenspace is the zero-charge monomial of the unordered mode-one pair occupation. Repeated colours are included.

Theorem 1.9 (Literal charged orbit basis vectors).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.actualFixedEnergyTwoBasis_charge_coe

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.actualFixedEnergyTwoBasis_charge_coe (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

For positive definite rootless even LatticeData, each charged basis vector in the actual canonical fixed eigenspace is the sum of the two charged ground states at the chosen charge and its negative. Independence and spanning come from the constructed equivalence, rather than an orbit dimension assumption.

Theorem 1.10 (Actual fixed low-energy spectrum in arbitrary rank).

Lean statement: D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.actual_theta_fixed_rootless_low_spectrum

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/InvolutionRootlessLowGrades.actual_theta_fixed_rootless_low_spectrum (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Acknowledgement. Igor B. Frenkel, James Lepowsky, and Arne Meurman (1988). Vertex Operator Algebras and the Monster. DOI: 10.1016/S0079-8169(08)X6136-7.

Commentary.

For every even LatticeData whose real Gram matrix is positive definite and has no integral norm-two charges, the literal production fixedSpace intersections with the canonical inverse-Gram Sugawara L0 eigenspaces at energies zero, one and two have complex finranks one, zero, and choose(rank+1,2) plus Nat.card of the norm-four integral charge shell divided by two. Rank zero is included. The vacuum is fixed, every energy-one oscillator is odd, and energy two uses the constructed free charge-orbit basis. No trace, fixed dimension, shell count or convergence premise is used.

The reflection is the phase-one lift on the lattice vertex algebra. The reflection conjugacy relates the all-charge low-grade bases to the fixed orbit basis. Classical mathematical context is Frenkel-Lepowsky-Meurman, Vertex Operator Algebras and the Monster, and Bakalov-Kac, Twisted Modules over Lattice Vertex Algebras, arXiv math/0402315v1 section 4.1. Mathlib quotient, basis and symmetric-power APIs retain their original authorship and Apache-2.0 license. No literature novelty is claimed.

This constructs low-energy spaces of the existing fixed vertex algebra. It does not construct twisted sectors, an orbifold extension, a Monster action, fusion or anomaly data, string theory or an AdS/CFT bridge.

References