Weighted local extraction for the actual two branches
Abstract
Weighted local extraction for the actual two branches
Theorem 1.1 (Weighted local extraction for the actual two branches).
Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockSliceQuotient/WeightedExtraction.actual_two_branch_supplier
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockSliceQuotient/WeightedExtraction.actual_two_branch_supplier (✓ 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.
Commentary.
A finite Laurent numerator has a signed local collision formula with all weighted spectator poles retained. Shifting the numerator removes negative powers for partial-fraction decomposition; the origin contribution has zero collision jump, while each nonzero pole contributes its local residue.
The resulting weighted fiber identity identifies complete current/source local residues in the supported triple carriers. Combining it with the actual homogeneous Laurent carrier supplier and native current inverse gives both the actual J/A branch and the swapped J/B branch for one numerator and all signed modes. These two branches feed the arbitrary-cutoff quotient comparison; no finite Taylor identification is asserted.
Classical local-field provenance is Matsuo–Nagatomo and Bakalov–Kac (math/0402315). The source retains the mathlib Hahn/Laurent and partial-fraction authors and Scott Carnahan/vertexAlg composition attribution under Apache 2.0.