Supported complete nested residue readouts
Abstract
Supported complete nested residue readouts
Theorem 1.1 (Supported complete nested residue readouts).
Lean statement: D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockSliceQuotient/SupportedReadouts.supportedNestedLeftReadout_eq
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/NestedResidues/LatticeHalfFockSliceQuotient/SupportedReadouts.supportedNestedLeftReadout_eq (✓ 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.
The finite fractional product uses the lawful complete residue Calculus.Q. Its scalar readout is the signed forward-minus-reverse binomial residue, and full-field locality makes the complete outer residue sum equal to any sufficient cutoff.
The two supported inner pair extractions are computed coefficient by coefficient in the Hahn carriers. Their nested left and right formulas preserve the spectator modes and the same total signed mode. The left and swapped current/second-source computations are used together in the actual two-branch supplier. A finite cutoff on the fractional product does not assert separate support of either ordered residue term.
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.