All-source Physical Locality
Abstract
The canonical corrected field is local at one doubled-shift order for every pair of finite-charge sources.
For arbitrary integral symmetric even lattice data D, a determinant unit hu, sources first and second in the existing Carrier D, every signed integer exponent pair and every ActualTensor D hu state, one natural order is selected before the exponents and state. The displayed binomial sum of corrected-field coefficients at the even shifts 2*(order-offset) and 2*offset is zero.
The proof uses the existing charged coefficient locality supplier, direct signed physical slices and jets, canonical singleton insertion, uniform-shift Dong locality for repeated words, and the unchanged finite Corr/charge/basis expansion of correctedField. Finite support is used pointwise after fixing the actual tensor input; no positivity, homogeneity, source-product or extra locality premise is introduced.
Theorem 1.1 (Exact unrestricted all-source physical locality).
Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockAllStatePhysicalLocality.correctedField_physical_locality
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockAllStatePhysicalLocality.correctedField_physical_locality (✓ 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.
The witness order depends only on the two fixed sources and lattice data. It is chosen before all signed exponents and target vectors. The cover grid is the commutator of the two physical slices at shifts -E-2 and -F-2; finite linear closure over the actual charge, correction-shift and repeated monomial supports gives the corrected-field coefficient identity.
This algebraic result leaves source-product compatibility, twisted Jacobi, analytic CFT completion, fusion, string theory and AdS/CFT as separate obligations.