bibkey: matsuo1997locality authors: Atsushi Matsuo; Kiyokazu Nagatomo year: 1997 title: On axioms for a vertex algebra and the locality of quantum fields doi: null url: https://arxiv.org/abs/hep-th/9706118v1 claim: Pairwise local creative fields with a common translation operator reconstruct a vertex algebra; residue products preserve locality. strata_touched: [] license: citation-only triage: anchor

Local fields and reconstruction

Proposition 1.5.5, printed page 11, proves locality of residue products of pairwise local fields. For residue index minus one, the sum of the three pairwise orders is a sufficient locality order. These orders depend on the fields, not on the vector to which their modes are applied.

Theorem 5.2.1, printed page 33, includes lower truncation, all-state locality, creation and a common translation operator annihilating the vacuum among the reconstruction conditions. Theorem 5.4.1, printed page 35, reconstructs state fields from creative local generators, their vacuum-mode span and a common translation operator. Its construction uses divided derivatives and ordered normal products.

The polynomial Fock construction in PolynomialFockStateField.lean uses the actual current, sorts the monomial occurrences, explicitly right-nests normal products and extends by the monomial basis. This is an implementation of classical mathematics, not a claim of a new reconstruction theorem. The actual L(-1) translates every resulting field. The locality proof uses the finite-support residue boundary and the three-order binomial cancellation in FieldNormalProductLocality.lean; induction through arbitrary words and finite polynomial supports chooses an order independently of the input vector. The quadratic conformal state’s modes are the existing L(n-1). These field conditions do not supply a bundled Jacobi-identity interface. The reference does not supply Lean proof terms, an actual Monster realization or a spacetime reconstruction.

The rational polynomial model embeds through MvPolynomial.map (algebraMap ℚ ℂ). The map is injective, preserves every variable and the vacuum, and commutes with polynomial partial derivatives. Thus the rational creation operator X_k * p and annihilation operator (k+1) • pderiv k p map to the same complex operators used by the construction. Slot k represents the mode with creation index -(k+1), not a changed Heisenberg normalization.

Source adaptation

FieldNormalProduct.lean selectively adapts Hasse lifting and the finite support arguments, and PolynomialFockJacobi.lean uses the two active integer residue-support kernels inside its actual residue-field constructor, from Scott Carnahan’s VertexAlg/VertexBasic/VertexOperator.lean at revision 4453e34ec390e82a0c789c731ada8f9a6e86bdea of ScottCarnahan/vertexAlg. The original file’s SHA-256 is ec4e543a6411876f19638138f825668785f2f30ace3f30cbe9328640ac02a2e2. Its copyright header grants Apache-2.0 licensing; that revision’s recursive tree contains no LICENSE or NOTICE file. This repository’s root LICENSE provides the full Apache-2.0 terms. The adapted source preserves the original copyright and author notice and identifies its modifications.

The source pins Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474; this repository instead uses Lean 4.33.0 and Mathlib revision db584cd6d46c92f209a44c0f1c829460d327499d. The transplant reuses the latter’s LaurentSeries.hasseDeriv; it does not alter either dependency pin. The minus-one coefficient construction and the all-integer residue coefficients have bounded-pole arguments expressed using finitely many actual intermediate states. Residue coefficients use integer generalized binomial coefficients cast to the complex numbers and the integer power of minus one. The support kernels are local constructor facts, not separately frozen mathematical results. Covariance is proved by supported coefficient telescoping inside the actual residue-closure proof. The derivative and normal-product locality proofs are also developed here from coefficient functions, not attributed to an upstream compiled locality theorem.

Nonnegative residues use finite double-commutator cancellation in commuting coefficient shifts. Relative vacuum uniqueness requires locality only with the existing state fields, not membership in their image. The integer composition identity follows from residue closure, the high-residue locality region and the supported Pascal discrepancy recurrence, including negative integer indices.

Upstream derivative-locality and Dong locality statements are commented sketches, not compiled suppliers. No such sketch is copied as a theorem or assumed as an axiom. The transplant is retired only when direct use of equivalent declarations from this repository’s own pinned Mathlib compiles for the actual Fock consumer.

Verified locator

• Matsuo–Nagatomo, arXiv hep-th/9706118v1, PDF SHA-256 2e1dabebeffe511c8bd14c0a4e6449afefcf508a02135d96df2042a0ccca07ea, Lemma 1.5.4, Propositions 1.5.5 and 3.2.2, and Theorems 5.2.1 and 5.4.1: https://arxiv.org/abs/hep-th/9706118v1
• Carnahan source: https://github.com/ScottCarnahan/vertexAlg/blob/4453e34ec390e82a0c789c731ada8f9a6e86bdea/VertexAlg/VertexBasic/VertexOperator.lean

Power-state coefficient conventions

Sections 1.2 and 1.4 use the expansion $A(z)={\sum }_{n\in \mathbb{Z}}{A}_n{z}^{-n-1}$ and the lower truncation condition on each input vector. For the minus-one residual product, Section 1.4 gives

$$(A_{(-1)}B{)}_{n}v=\sum _{j\ge 0}{A}_{-j-1}{B}_{n+j}v+\sum _{j\ge 0}{B}_{n-j-1}{A}_{j}v.$$

Each branch is finite on the specified vector. The operator order is the order of the displayed products; normal products need not commute. In the complex polynomial realization, $Y(X_0^p)$ is the right-nested word of $p$ currents. Its coefficients on $X_0^q$ require evaluating those finite branches, the creation-series convolution, and the falling-factorial multiplicities. This realization calculation is a classical formalization contribution, not a new abstract Wick theorem.

Tong, String Theory, Section 4.3.3, printed pages 80–82, explains summing over pair contractions and gives multiplicities 2 and 4 in the stress-tensor example, equation (4.28): https://davidtong.org/pdfs/teaching/string-theory/string4.pdf . His holomorphic derivative contraction is $-{\alpha }^{\prime }/2$ times the inverse squared separation. This is background for pairing counts, not an exact source for the all-integer polynomial output formula with the unit Heisenberg normalization.