Actual half-Sugawara boundary, shift and spectrum

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.

The direct central proof computes the normal cutoff change, proves finite support for its scalar boundary for every integer sign, reindexes only the actual finite sums, and contracts inverse-Gram trace to rank. It does not use a scalar-rigidity branch or import the research Sugawara excerpt.

Support for p and rawL_m p is established separately in the mixed normal-sum calculation. The scalar term sum_j (j+1/2)(m+j+1/2)(1_(j>=0)-1_(m+j>=0)) equals (2m^3+m)/12 and is consumed by the actual operator contraction.

Creation multiplication at variable (i,k) raises L0 energy by k+1/2. Power induction and finite exponent-vector induction prove the monomial law; linearity extends it to arbitrary finite sums. Ground need not be a VOA vacuum.

Theorem 1.1 (Actual raw central term for all integers).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.rawL_virasoro

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.rawL_virasoro (✓ 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) (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)))) (m n : 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.rawL D H n)) (@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 n) (D5.S3.VertexAlgebra.LatticeHalfFock.rawL D H m))) (@HAdd.hAdd.{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))) (@instHAdd.{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.instAdd.{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)))) (@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))))) (@HSub.hSub.{0, 0, 0} Complex Complex Complex (@instHSub.{0} Complex Complex.instSub) (@Int.cast.{0} Complex Complex.instIntCast m) (@Int.cast.{0} Complex Complex.instIntCast n)) (D5.S3.VertexAlgebra.LatticeHalfFock.rawL D H (@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd) m n))) (@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) m n) (@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) m n) (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))) (@HDiv.hDiv.{0, 0, 0} Complex Complex Complex (@instHDiv.{0} Complex (@DivInvMonoid.toDiv.{0} Complex Complex.instDivInvMonoid)) (@HMul.hMul.{0, 0, 0} Complex Complex Complex (@instHMul.{0} Complex Complex.instMul) (@Nat.cast.{0} Complex Complex.instNatCast (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (@HAdd.hAdd.{0, 0, 0} Complex Complex Complex (@instHAdd.{0} Complex Complex.instAdd) (@HMul.hMul.{0, 0, 0} Complex Complex Complex (@instHMul.{0} Complex Complex.instMul) (@OfNat.ofNat.{0} Complex (nat_lit 2) (@instOfNatAtLeastTwo.{0} Complex (nat_lit 2) Complex.instNatCast (@Nat.instAtLeastTwoHAddOfNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) (@Nat.instNeZeroSucc (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))))) (@HPow.hPow.{0, 0, 0} Complex Nat Complex (@instHPow.{0, 0} Complex Nat (@NPow.toPow.{0} Complex (@Monoid.toNPow.{0} Complex (@Semiring.toMonoid.{0} Complex Complex.instSemiring)))) (@Int.cast.{0} Complex Complex.instIntCast m) (@OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3))))) (@Int.cast.{0} Complex Complex.instIntCast m))) (@OfNat.ofNat.{0} Complex (nat_lit 24) (@instOfNatAtLeastTwo.{0} Complex (nat_lit 24) Complex.instNatCast (@Nat.instAtLeastTwoHAddOfNat (@OfNat.ofNat.{0} Nat (nat_lit 23) (instOfNatNat (nat_lit 23))) (@Nat.instNeZeroSucc (@OfNat.ofNat.{0} Nat (nat_lit 22) (instOfNatNat (nat_lit 22)))))))) (@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)))))))

Assuming exactly HGc=GcH=1, [rawL_m,rawL_n]=(m-n)rawL_(m+n)+delta_(m+n,0)rank(2m^3+m)/24 identity, all integers m,n and all ranks including zero.

Theorem 1.2 (Actual half-Casimir ground contraction).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.positive_ground_boundary

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

Source. Repository-derived.

Commentary.

For each natural m, rawL_m(rawL_-m 1)=(rank/2) sum_(k=0..m-1)(k+1/2)(m-k-1/2) times 1, under the same inverse pair. The operator connection follows from the actual raw Virasoro calculation and raw nonnegative-ground vanishing.

Theorem 1.3 (Rank/16 is forced by the actual first contraction).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.shift_forced

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

Source. Repository-derived.

Commentary.

For any complex h, if the actual raw commutator [rawL_1,rawL_-1]1=2h times 1, then h=rank/16. The actual m=1 defect is rank/8. This normalization condition is used only for this uniqueness conclusion and is never a premise of the representation or Virasoro relation.

Theorem 1.4 (Shifted rank-central-charge Virasoro law).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.L_virasoro

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.L_virasoro (✓ 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)))) (m n : 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.L D H m) (D5.S3.VertexAlgebra.LatticeHalfFock.L D H n)) (@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.L D H n) (D5.S3.VertexAlgebra.LatticeHalfFock.L D H m))) (@HAdd.hAdd.{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))) (@instHAdd.{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.instAdd.{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)))) (@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))))) (@HSub.hSub.{0, 0, 0} Complex Complex Complex (@instHSub.{0} Complex Complex.instSub) (@Int.cast.{0} Complex Complex.instIntCast m) (@Int.cast.{0} Complex Complex.instIntCast n)) (D5.S3.VertexAlgebra.LatticeHalfFock.L D H (@HAdd.hAdd.{0, 0, 0} Int Int Int (@instHAdd.{0} Int Int.instAdd) m n))) (@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) m n) (@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) m n) (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))) (@HMul.hMul.{0, 0, 0} Complex Complex Complex (@instHMul.{0} Complex Complex.instMul) (@HDiv.hDiv.{0, 0, 0} Complex Complex Complex (@instHDiv.{0} Complex (@DivInvMonoid.toDiv.{0} Complex Complex.instDivInvMonoid)) (@Nat.cast.{0} Complex Complex.instNatCast (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (@OfNat.ofNat.{0} Complex (nat_lit 12) (@instOfNatAtLeastTwo.{0} Complex (nat_lit 12) Complex.instNatCast (@Nat.instAtLeastTwoHAddOfNat (@OfNat.ofNat.{0} Nat (nat_lit 11) (instOfNatNat (nat_lit 11))) (@Nat.instNeZeroSucc (@OfNat.ofNat.{0} Nat (nat_lit 10) (instOfNatNat (nat_lit 10)))))))) (@HSub.hSub.{0, 0, 0} Complex Complex Complex (@instHSub.{0} Complex Complex.instSub) (@HPow.hPow.{0, 0, 0} Complex Nat Complex (@instHPow.{0, 0} Complex Nat (@NPow.toPow.{0} Complex (@Monoid.toNPow.{0} Complex (@Semiring.toMonoid.{0} Complex Complex.instSemiring)))) (@Int.cast.{0} Complex Complex.instIntCast m) (@OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))) (@Int.cast.{0} Complex Complex.instIntCast m))) (@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)))))))

The constructed shifted End operators satisfy [L_m,L_n]=(m-n)L_(m+n)+delta_(m+n,0)(rank/12)(m^3-m) identity, under exactly the two inverse equations, for all integers m,n and ranks including zero.

Theorem 1.5 (Exact actual monomial spectrum).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.L_zero_monomial_coeff

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

Source. Repository-derived.

Commentary.

For every finite exponent vector d and arbitrary complex coefficient c, L_0(monomial d c)=(rank/16+sum_(x in support(d)) d(x)(x.2+1/2)) times monomial d c, under the same inverse pair. Neither weighted homogeneity nor an eigenvector premise is assumed.

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/LatticeHalfFockVirasoroSpectrum.L_virasoro
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.L_zero_monomial_coeff
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.positive_ground_boundary
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.rawL_virasoro
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum.shift_forced
Dependency: D5/S3/VertexAlgebra/LatticeHalfFockCurrentNormal

Keyboard shortcuts

trureturing — Discovering truth

Actual half-Sugawara boundary, shift and spectrum

Abstract

References