FiniteChambers
Abstract
Supported formal collision residues.
Theorem 1.1 (The two finite ordered contraction sums).
Lean statement: D5/S3/VertexAlgebra/ChargedResidue/FiniteChambers.native_chamber_scalar_full
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/ChargedResidue/FiniteChambers.native_chamber_scalar_full (✓ 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.
Each contraction chamber has its own natural range. A supported sparse quadratic convolution identifies each ordered sum with its signed chamber coefficient. The signed difference is evaluated by the two-pole formula, keeping both negative-degree tests. The identity is used in the actual complete residue diagonal for arbitrary translated input monomials.