Actual half currents and finite Sugawara normal sums

Abstract

Let D have natural rank, an integral symmetric Gram matrix G and even diagonal. Rank zero is included. P is the actual complex MvPolynomial on Fin(rank(D)) times N. No positivity or unimodularity is assumed. Current Heisenberg and support results require no inverse matrix.

Write Gc=D.G.map(Int.cast). Sugawara commutator, central and spectrum laws assume exactly HGc=1 and GcH=1. Symmetry of H is derived from these two identities and symmetry of G; it is not an additional premise. No desired current or Virasoro law, grading or homogeneity is assumed.

For integer j the physical frequency is j+1/2 and the opposite parameter is -j-1; there is no zero-frequency mode. Negative j acts by multiplication by X(i,(-j-1).toNat). Nonnegative j acts by (j+1/2) times the actual Gram-weighted polynomial derivative.

R(p) is the supremum of k+1 over variables actually appearing in p. Normal pairs use the physical creation-left split j<0, including j=-1. Their finite support is established before forming the linear End operator normalSum. rawL_m=(1/2) sum_i,l H_i,l normalSum_i,l(m). L_m=rawL_m+delta_(m,0) rank/16 identity; the second host proves that shift is forced by the actual contraction.

Theorem 1.1 (Actual all-integer Heisenberg law).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.current_heisenberg

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.current_heisenberg (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kalle Kytölä (2025). VirasoroProject, Sugawara.lean. URL: https://github.com/kkytola/VirasoroProject/blob/5ff4245383b2cdd4eea7a0524bc1274c32041eb4/VirasoroProject/Sugawara.lean.

Commentary.

Exact currently loaded native universal type: ∀ (D : D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData) (i l : Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (j k : Int), @Eq.{1} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@HSub.hSub.{0, 0, 0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHSub.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@LinearMap.instSub.{0, 0, 0, 0} Complex Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.addCommGroup.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instRing) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring)))) (@HMul.hMul.{0, 0, 0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHMul.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.instMul.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)))) (D5.S3.VertexAlgebra.LatticeHalfFock.current D i j) (D5.S3.VertexAlgebra.LatticeHalfFock.current D l k)) (@HMul.hMul.{0, 0, 0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHMul.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.instMul.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)))) (D5.S3.VertexAlgebra.LatticeHalfFock.current D l k) (D5.S3.VertexAlgebra.LatticeHalfFock.current D i j))) (@HSMul.hSMul.{0, 0, 0} Complex (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHSMul.{0, 0} Complex (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@LinearMap.instSMul.{0, 0, 0, 0, 0} Complex Complex Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring)) (@AddMonoidAlgebra.distribSMul.{0, 0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@NonUnitalNonAssocSemiring.toDistribSMul.{0} Complex (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing.{0} Complex (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{0} Complex Complex.instNonUnitalCommRing))))) (@AddMonoidAlgebra.smulCommClass.{0, 0, 0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@DistribSMul.toSMulZeroClass.{0, 0} Complex Complex (@AddMonoid.toAddZeroClass.{0} Complex (@AddMonoidWithOne.toAddMonoid.{0} Complex (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Complex (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)))))) (@DistribMulAction.toDistribSMul.{0, 0} Complex Complex (@Semiring.toMonoid.{0} Complex Complex.instSemiring) (@AddMonoidWithOne.toAddMonoid.{0} Complex (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Complex (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))))) (@Module.toDistribMulAction.{0, 0} Complex Complex Complex.instSemiring (@Semiring.toAddCommMonoid.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@Semiring.toModule.{0} Complex Complex.instSemiring)))) (@DistribSMul.toSMulZeroClass.{0, 0} Complex Complex (@AddMonoid.toAddZeroClass.{0} Complex (@AddMonoidWithOne.toAddMonoid.{0} Complex (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Complex (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)))))) (@NonUnitalNonAssocSemiring.toDistribSMul.{0} Complex (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing.{0} Complex (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{0} Complex Complex.instNonUnitalCommRing))))) (@Algebra.to_smulCommClass.{0, 0} Complex Complex Complex.instCommSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Algebra.id.{0} Complex Complex.instCommSemiring))))) (@ite.{1} Complex (@Eq.{1} Int (@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd) (@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd) j k) (@OfNat.ofNat.{0} Int (nat_lit 1) (@instOfNat (nat_lit 1)))) (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))) (Int.instDecidableEq (@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd) (@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd) j k) (@OfNat.ofNat.{0} Int (nat_lit 1) (@instOfNat (nat_lit 1)))) (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))) (@HMul.hMul.{0, 0, 0} Complex Complex Complex (@instHMul.{0} Complex Complex.instMul) (D5.S3.VertexAlgebra.LatticeHalfFock.frequency j) (@Int.cast.{0} Complex Complex.instIntCast (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.G D i l))) (@OfNat.ofNat.{0} Complex (nat_lit 0) (@Zero.toOfNat0.{0} Complex Complex.instZero))) (@OfNat.ofNat.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (nat_lit 1) (@One.toOfNat1.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.instOne.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))))))

For every colour i,l and integers j,k, [a_i(j),a_l(k)]=delta_(j+k+1,0)(j+1/2)G_i,l identity on P. Four integer sign cases are proved on arbitrary polynomials. Only symmetry of G is used.

Theorem 1.2 (Actual variable-frequency truncation).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.current_vanish

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.current_vanish (✓ std3). ∎

Source. Repository-derived.

Commentary.

Exact currently loaded native universal type: ∀ (D : D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData) (i : Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (p : D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (j : Int) (hj : @LE.le.{0} Int Int.instLEInt (@Nat.cast.{0} Int instNatCastInt (D5.S3.VertexAlgebra.LatticeHalfFock.bound D p)) j), @Eq.{1} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (@DFunLike.coe.{1, 1, 1} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (fun (x : D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) => D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (@LinearMap.instFunLike.{0, 0, 0, 0} Complex Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring))) (D5.S3.VertexAlgebra.LatticeHalfFock.current D i j) p) (@OfNat.ofNat.{0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (nat_lit 0) (@Zero.toOfNat0.{0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (@MulZeroClass.toZero.{0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (@instMulZeroClassOfSemiring.{0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (@AddMonoidAlgebra.semiring.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Finsupp.instAddMonoid.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat Nat.instAddMonoid))))))

For arbitrary polynomial p and j>=R(p), a_i(j)p=0. This derives support from the actual input variables, including nonhomogeneous p.

Theorem 1.3 (Finite physical normal support).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.normalPair_support_interval

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.normalPair_support_interval (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every integer m and p, support of j -> normalPair_i,l(j,m-j-1)p is contained in Icc(min(m-R(p),0),R(p)-1). Bounds apply to the rightmost actual input.

Theorem 1.4 (Cutoff independence on each input).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.normalSum_interval

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.normalSum_interval (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite interval [a,b] with a<=min(m-R(p),0) and b>=R(p)-1 computes exactly normalSum_i,l(m)p. This is an equality of the constructed finite sum value, with no uniform cutoff assumption.

Theorem 1.5 (Actual high raw modes vanish).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_truncation

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_truncation (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary H,p and integer m>=2R(p), rawL_m p=0. When both currents annihilate, their genuine commutator is used before applying the input support bound.

Theorem 1.6 (All negative ground modes are finite creation polynomials).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_ground_negative

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_ground_negative (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every H and integer m<0, rawL_m 1=(1/2) sum_i,l H_i,l sum_(j in Icc(m,-1)) X(i,(-j-1).toNat) X(l,(j-m).toNat). No inverse equation is required for this creation formula.

Theorem 1.7 (Actual all-integer Sugawara-current law).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_current_commutator

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_current_commutator (✓ std3). ∎

Source. Repository-derived.

Commentary.

Exact currently loaded native universal type: ∀ (D : D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData) (H : Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (hHG : @Eq.{1} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (@HMul.hMul.{0, 0, 0} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (@Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.{0, 0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex (Fin.fintype (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex.instMul Complex.instAddCommMonoid) H (D5.S3.VertexAlgebra.LatticeHalfFock.gramComplex D)) (@OfNat.ofNat.{0} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (nat_lit 1) (@One.toOfNat1.{0} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (@Matrix.one.{0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex (instDecidableEqFin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex.instZero Complex.instOne)))) (hGH : @Eq.{1} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (@HMul.hMul.{0, 0, 0} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (@Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.{0, 0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex (Fin.fintype (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex.instMul Complex.instAddCommMonoid) (D5.S3.VertexAlgebra.LatticeHalfFock.gramComplex D) H) (@OfNat.ofNat.{0} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (nat_lit 1) (@One.toOfNat1.{0} (Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (@Matrix.one.{0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex (instDecidableEqFin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex.instZero Complex.instOne)))) (a : Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (m q : Int), @Eq.{1} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@HSub.hSub.{0, 0, 0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHSub.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@LinearMap.instSub.{0, 0, 0, 0} Complex Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.addCommGroup.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instRing) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring)))) (@HMul.hMul.{0, 0, 0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHMul.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.instMul.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)))) (D5.S3.VertexAlgebra.LatticeHalfFock.rawL D H m) (D5.S3.VertexAlgebra.LatticeHalfFock.current D a q)) (@HMul.hMul.{0, 0, 0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHMul.{0} (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.instMul.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)))) (D5.S3.VertexAlgebra.LatticeHalfFock.current D a q) (D5.S3.VertexAlgebra.LatticeHalfFock.rawL D H m))) (@HSMul.hSMul.{0, 0, 0} Complex (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@instHSMul.{0, 0} Complex (@Module.End.{0, 0} Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring))) (@LinearMap.instSMul.{0, 0, 0, 0, 0} Complex Complex Complex (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) Complex.instSemiring Complex.instSemiring (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instAddCommMonoid.{0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex.instSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex Complex.instSemiring)) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring)) (@AddMonoidAlgebra.distribSMul.{0, 0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@NonUnitalNonAssocSemiring.toDistribSMul.{0} Complex (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing.{0} Complex (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{0} Complex Complex.instNonUnitalCommRing))))) (@AddMonoidAlgebra.smulCommClass.{0, 0, 0, 0} Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) Complex Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@DistribSMul.toSMulZeroClass.{0, 0} Complex Complex (@AddMonoid.toAddZeroClass.{0} Complex (@AddMonoidWithOne.toAddMonoid.{0} Complex (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Complex (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)))))) (@DistribMulAction.toDistribSMul.{0, 0} Complex Complex (@Semiring.toMonoid.{0} Complex Complex.instSemiring) (@AddMonoidWithOne.toAddMonoid.{0} Complex (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Complex (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))))) (@Module.toDistribMulAction.{0, 0} Complex Complex Complex.instSemiring (@Semiring.toAddCommMonoid.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)) (@Semiring.toModule.{0} Complex Complex.instSemiring)))) (@DistribSMul.toSMulZeroClass.{0, 0} Complex Complex (@AddMonoid.toAddZeroClass.{0} Complex (@AddMonoidWithOne.toAddMonoid.{0} Complex (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Complex (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring)))))) (@NonUnitalNonAssocSemiring.toDistribSMul.{0} Complex (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{0} Complex (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing.{0} Complex (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{0} Complex Complex.instNonUnitalCommRing))))) (@Algebra.to_smulCommClass.{0, 0} Complex Complex Complex.instCommSemiring (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Algebra.id.{0} Complex Complex.instCommSemiring))))) (@Neg.neg.{0} Complex Complex.instNeg (D5.S3.VertexAlgebra.LatticeHalfFock.frequency q)) (D5.S3.VertexAlgebra.LatticeHalfFock.current D a (@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd) m q)))

Under precisely HGc=GcH=1, [rawL_m,a_i(q)]=-(q+1/2)a_i(m+q), for all integers m,q. The two exceptional finite contractions occur at j=m+q and j=-q-1. Support is proved separately for p and a_i(q)p.

Bakalov-Kac, Twisted Modules over Lattice Vertex Algebras, arXiv math/0402315v1 (2004-02-19): PDF p.8 (4.4), pp.10-13 (4.23),(4.26)-(4.38) give the current, half-field and normalization context. Its pp.4-7 (3.1)-(3.7),(3.13),(3.18)-(3.19), Proposition 3.1 and p.14 Proposition 4.2 concern the still-open fractional products and full twisted reconstruction; those results are not asserted by this unit.

Dong-Nagatomo, Automorphism Groups and Twisted Modules for Lattice Vertex Operator Algebras, arXiv math/9808088v1 (1998-08-19), section 3.2 PDF pp.12-14, especially the displayed oscillator tensor ground and Delta on p.13. Rank/16 is stated in the proof of Theorem 3.13(3), p.19 (the theorem begins on p.18), and is credited there to FLM. This is DN-to-FLM attribution only: neither the FLM nor FHL full text was retrieved.

The finite normal-boundary, current-contraction and induction architecture acknowledges Kalle Kytola, VirasoroProject revision 5ff4245383b2cdd4eea7a0524bc1274c32041eb4, Apache-2.0, through the inspected completed PolynomialFock sources at trureturing revision bfd9ff0f15397a4fb933f36d701a60d325d84b08. The kytola2025virasoro library note identifies this pinned architecture, not an already formalized multicolour half-mode theorem. Formal proof provenance is repo-derived with this acknowledgement.

The existing flm1988monster library note is associated only as a bibliographic and ordinary-lattice background anchor. It is not proof origin for an uninspected FLM or FHL theorem or for the new half-mode matrix proof. The exact BK and DN locators above supply the literature input.

DN p.13 displays a c_mn integrality assertion conflicting with its displayed logarithmic generating function. For F(x,y)=-log((sqrt(1+x)+sqrt(1+y))/2), write its logarithm argument as 1+(x+y)/4-(xx+yy)/16 plus terms of total degree at least three. The expansion -log(1+u)=-u+uu/2 plus higher terms gives F=-(x+y)/4+3(xx+yy)/32+x*y/16 plus higher terms. Thus c10=c01=-1/4 and c11=1/16 are rational. Ordered m,n coefficients and their derivatives must retain both ordered mixed contributions. This is a derived correction, not a published erratum and not an implemented Delta operator.

Charged theta fields, corrected fractional normal products, all-state twisted locality/Jacobi, Y_theta(omega) identification, twisted intertwiners, holomorphic extension, Leech/Monster, anomaly/fusion, full CFT, string theory and the AdS/CFT bridge remain subsequent obligations.

D5/L/VertexAlgebra/flm1988monster

References

Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.current_heisenberg
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.current_vanish
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.normalPair_support_interval
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.normalSum_interval
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_current_commutator
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_ground_negative
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal.rawL_truncation
Dependency: D5/S3/VertexAlgebra/LatticeActualAnnihilation

Keyboard shortcuts

trureturing — Discovering truth

Actual half currents and finite Sugawara normal sums

Abstract

References