SupportedResidue
Abstract
Supported formal collision residues.
Theorem 1.1 (The actual residue on the common collision diagonal).
Lean statement: D5/S3/VertexAlgebra/ChargedResidue/SupportedResidue.chargedPhysicalResidueRow_collision_diagonal
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/ChargedResidue/SupportedResidue.chargedPhysicalResidueRow_collision_diagonal (✓ std3). ∎
Source. Repository-derived.
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 original lattice, unit determinant, charges, signs, matching integer lifts and signed indices, the complete physical residue on an arbitrary oscillator tensor an actual ground vector equals the sum over its genuine pair-translated polynomial support with the two-pole scalar weights. Each whole ordered sum is enlarged by its own field order before monomial expansion. The two scalar chambers are then combined; neither ordered half is asserted to vanish.