Ordered Normal Products
Abstract
Ordered normal products preserve mode translation covariance.
The product has two pointwise finite coefficient sums. Its truncation uses the right field on the input and on finitely many actual intermediate states of the left field. Hasse lifting and support arguments adapt Carnahan’s licensed original source; no unproved locality supplier is imported.
Theorem 1.1 (Translation covariance passes through the ordered product).
Lean statement: D5/S3/VertexAlgebra/FieldNormalProduct.normalMinusOne_translation
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FieldNormalProduct.normalMinusOne_translation (✓ std3). ∎
Citation. Atsushi Matsuo; Kiyokazu Nagatomo (1997). On axioms for a vertex algebra and the locality of quantum fields. URL: https://arxiv.org/abs/hep-th/9706118v1.
Commentary.
For any complex module, any actual endomorphism T and two fields whose nth modes satisfy [T,A_n]=-n A_(n-1), the ordered minus-one product satisfies the same relation. The proof shifts the two finite sums across their zero-mode boundary. It asserts covariance, not locality.
References
- Truth anchor:
D5/S3/VertexAlgebra/FieldNormalProduct.normalMinusOne_translation