Actual arbitrary-ground tensor operators and supported half fields

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.

Let T be any Type with AddCommGroup T and Module Complex T, with no finite-dimensional, irreducible or Nontrivial premise. tensorEnd(A) is the actual TensorProduct.map A id. tensorCurrent, tensorRawL and tensorL are these actual operators. Tensor induction gives contextual current and stress bounds on every actual tensor vector, including arbitrary sums of pure tensors.

The tensor current and Virasoro laws follow by actual TensorProduct.map transport of the retained operator equalities. On P tensor T the current central factor is delta_(j+k+1,0)(j+1/2)G_i,l and the shifted Virasoro central factor is delta_(m+n,0)(rank/12)(m^3-m). There is no scalar-commutant assertion on P tensor T.

The same actual transport gives the monomial tensor energy, L_0(1 tensor t)=rank/16 (1 tensor t), all positive L_m(1 tensor t)=0, and all negative ground finite creation formulas from the first host. In particular L_-1(1 tensor t)=(1/2 sum_i,l H_i,l X(i,0)X(l,0)) tensor t. It generally is nonzero: rank-one G=2,H=1/2 gives (1/4)X(0,0)^2. This ground state differs from a VOA vacuum.

HalfField is HVertexOperator on integer exponents in t=sqrt(z). The supported actual currentField and tensorCurrentField have coefficient -2j-3 equal to the physical current with index j. The supported actual stressField and tensorStressField have coefficient -2m-4 equal to the shifted L_m. There is no Y_theta(omega) identity or assumed all-state twisted Y.

At rank zero, the current colour is empty and the modes, shift and stress fields vanish.

Theorem 1.1 (The original tensor normal pair).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensorPair_eq

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

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

Visibility-only exposure of the original two normal-order branches, with the proof body unchanged. ActualMobiusCovariance charged_pair_l1 consumes the equality for j and -j, retaining the j=0 boundary.

Theorem 1.2 (Pointwise finite support of the original tensor pair).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensorPair_finite

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

Source. Repository-derived.

Acknowledgement. Bojko Bakalov and Victor G. Kac (2004). Twisted Modules over Lattice Vertex Algebras. DOI: 10.1142/9789812702562_0001. URL: https://arxiv.org/abs/math/0402315v1.

Commentary.

Visibility-only exposure, statement and proof body unchanged. The charged normal-sum calculation applies the finite-support theorem only at an actual input x or chargedCoefficient(e)(x), never as finite support of endomorphism-valued modes.

Theorem 1.3 (Finite support on an arbitrary actual tensor vector).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensorPair_support_of_bound

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensorPair_support_of_bound (✓ 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) (T : Type u_1) [inst : AddCommGroup.{u_1} T] [inst_1 : @root.Module.{0, u_1} Complex T Complex.instSemiring (@AddCommGroup.toAddCommMonoid.{u_1} T inst)] (i l : Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (m : Int) (v : @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (R : Nat) (hR : ∀ (a : Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (j : Int), @LE.le.{0} Int Int.instLEInt (@Nat.cast.{0} Int instNatCastInt R) j → @Eq.{u_1 + 1} (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@DFunLike.coe.{u_1 + 1, u_1 + 1, u_1 + 1} (@Module.End.{0, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1)) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (fun (x : @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) => @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@LinearMap.instFunLike.{0, 0, u_1, u_1} Complex Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring))) (@D5.S3.VertexAlgebra.LatticeHalfFock.tensorCurrent.{u_1} D T inst inst_1 a j) v) (@OfNat.ofNat.{u_1} (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (nat_lit 0) (@Zero.toOfNat0.{u_1} (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@instZeroTensorProduct.{0, u_1, 0} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1)))), @LE.le.{0} (Set.{0} Int) (@Set.instLE.{0} Int) (@Function.support.{0, u_1} Int (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@instZeroTensorProduct.{0, u_1, 0} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) fun (j : Int) => @DFunLike.coe.{u_1 + 1, u_1 + 1, u_1 + 1} (@Module.End.{0, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1)) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (fun (x : @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) => @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@LinearMap.instFunLike.{0, 0, u_1, u_1} Complex Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring))) (@D5.S3.VertexAlgebra.LatticeHalfFock.tensorPair.{u_1} D T inst inst_1 i l j (@HSub.hSub.{0, 0, 0} Int Int Int (@instHSub.{0} Int Int.instSub) (@HSub.hSub.{0, 0, 0} Int Int Int (@instHSub.{0} Int Int.instSub) m j) (@OfNat.ofNat.{0} Int (nat_lit 1) (@instOfNat (nat_lit 1))))) v) (@Set.Icc.{0} Int (@PartialOrder.toPreorder.{0} Int (@ConditionallyCompletePartialOrderSup.toPartialOrder.{0} Int (@ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup.{0} Int (@ConditionallyCompleteLattice.toConditionallyCompletePartialOrder.{0} Int (@ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice.{0} Int Int.instConditionallyCompleteLinearOrder))))) (@Min.min.{0} Int Int.instMin (@HSub.hSub.{0, 0, 0} Int Int Int (@instHSub.{0} Int Int.instSub) m (@Nat.cast.{0} Int instNatCastInt R)) (@OfNat.ofNat.{0} Int (nat_lit 0) (@instOfNat (nat_lit 0)))) (@HSub.hSub.{0, 0, 0} Int Int Int (@instHSub.{0} Int Int.instSub) (@Nat.cast.{0} Int instNatCastInt R) (@OfNat.ofNat.{0} Int (nat_lit 1) (@instOfNat (nat_lit 1)))))

For every v in P tensor T, any actual current bound R for v gives support of j -> tensorPair_i,l(j,m-j-1)v contained in Icc(min(m-R,0),R-1). Such an R exists by tensor induction; no scalar-current-commutant or finite-dimensional premise is used.

Theorem 1.4 (Tensor operator agrees with its actual finite normal sum).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensor_rawL_finsum

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

Source. Repository-derived.

Commentary.

Exact currently loaded native universal type: ∀ (D : D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData) (T : Type u_1) [inst : AddCommGroup.{u_1} T] [inst_1 : @root.Module.{0, u_1} Complex T Complex.instSemiring (@AddCommGroup.toAddCommMonoid.{u_1} T inst)] (H : Matrix.{0, 0, 0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) Complex) (m : Int) (v : @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1), @Eq.{u_1 + 1} (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@DFunLike.coe.{u_1 + 1, u_1 + 1, u_1 + 1} (@Module.End.{0, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1)) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (fun (x : @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) => @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@LinearMap.instFunLike.{0, 0, u_1, u_1} Complex Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring))) (@D5.S3.VertexAlgebra.LatticeHalfFock.tensorRawL.{u_1} D T inst inst_1 H m) v) (@HSMul.hSMul.{0, u_1, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@instHSMul.{0, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instSMul.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1)) (@Inv.inv.{0} Complex Complex.instInv (@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)))))))) (@Finset.sum.{0, u_1} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@Finset.univ.{0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin.fintype (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D))) fun (i : Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) => @Finset.sum.{0, u_1} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@Finset.univ.{0} (Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) (Fin.fintype (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D))) fun (l : Fin (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.LatticeData.rank D)) => @HSMul.hSMul.{0, u_1, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@instHSMul.{0, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instSMul.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1)) (H i l) (@finsum.{u_1, 1} (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Int (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) fun (j : Int) => @DFunLike.coe.{u_1 + 1, u_1 + 1, u_1 + 1} (@Module.End.{0, u_1} Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1)) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (fun (x : @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) => @TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@LinearMap.instFunLike.{0, 0, u_1, u_1} Complex Complex (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) Complex.instSemiring Complex.instSemiring (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.addCommMonoid.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@TensorProduct.instModule.{0, 0, u_1} Complex Complex.instCommSemiring (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Oscillator D) T (@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)) (@AddCommGroup.toAddCommMonoid.{u_1} T inst) (@AddMonoidAlgebra.instModule.{0, 0, 0} Complex Complex (@Finsupp.{0, 0} (D5.S3.VertexAlgebra.LatticeGeneratingFieldLocality.Index D) Nat (@MulZeroClass.toZero.{0} Nat Nat.instMulZeroClass)) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring) (@Semiring.toModule.{0} Complex (@CommSemiring.toSemiring.{0} Complex Complex.instCommSemiring))) inst_1) (@RingHom.id.{0} Complex (@Semiring.toNonAssocSemiring.{0} Complex Complex.instSemiring))) (@D5.S3.VertexAlgebra.LatticeHalfFock.tensorPair.{u_1} D T inst inst_1 i l j (@HSub.hSub.{0, 0, 0} Int Int Int (@instHSub.{0} Int Int.instSub) (@HSub.hSub.{0, 0, 0} Int Int Int (@instHSub.{0} Int Int.instSub) m j) (@OfNat.ofNat.{0} Int (nat_lit 1) (@instOfNat (nat_lit 1))))) v)))

For every actual tensor vector v, tensorRawL_m v=(1/2) sum_i,l H_i,l finsum_j tensorPair_i,l(j,m-j-1)v. Tensor normalSum is constructed after finite support and proved equal to the mapped polynomial normalSum, so this formula is not a merely named transport.

Theorem 1.5 (Contextual stress truncation for arbitrary tensor inputs).

Lean statement: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensor_L_truncation

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

Source. Repository-derived.

Commentary.

For every v in P tensor T and arbitrary H, there is a natural R such that m>R implies tensorL_m v=0. Pure tensors use 2R(p); sums use the maximum. This is the actual support proof consumed by tensorStressField construction.

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/LatticeHalfFockTensorFields.tensorPair_eq
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensorPair_finite
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensorPair_support_of_bound
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensor_L_truncation
Truth anchor: D5/S3/VertexAlgebra/LatticeHalfFockTensorFields.tensor_rawL_finsum
Dependency: D5/S3/VertexAlgebra/LatticeHalfFockVirasoroSpectrum

Keyboard shortcuts

trureturing — Discovering truth

Actual arbitrary-ground tensor operators and supported half fields

Abstract

References