Signed normal-product locality
Abstract
Signed normal-product locality
The finite-support constructions and residue telescope retain the Scott Carnahan vertexAlg Apache-2.0 attribution of their existing suppliers. The signed proof calculations adapt the actual bc ghost supplier to arbitrary complex modules, while reusing the existing generic PairSpace cancellation kernel and delta-binomial identity. This is classical Dong locality and creative reconstruction, with no literature novelty claim.
Theorem 1.1 (Independent signs and uniform residue cancellation).
Lean statement: D5/S3/VertexAlgebra/SignedFields/SignedFieldNormalProductLocality.signedNormal_locality
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/SignedFields/SignedFieldNormalProductLocality.signedNormal_locality (✓ std3). ∎
Source. Repository-derived.
Commentary.
For arbitrary complex modules and three fields A,B,C, locality with independent signs x,y,z implies locality of the signed normal product with C and sign yz. The order is Na+Nb+Nc, independent of every input vector. The signed triple pair has the two annihilators required by the existing PairSpace cancellation kernel.
Theorem 1.2 (Every divided derivative preserves the sign).
Lean statement: D5/S3/VertexAlgebra/SignedFields/SignedFieldNormalProductLocality.signedDerivative_locality
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/SignedFields/SignedFieldNormalProductLocality.signedDerivative_locality (✓ std3). ∎
Source. Repository-derived.
Commentary.
The degree d divided derivative of A has locality order N+d against B, with the original sign. A finite-difference Leibniz calculation and the derivative/factorial identity establish the bound. No global support of endomorphism families is assumed.