Original corrected field energy covariance

Abstract

The theorem uses exactly the original correctedField and actualTensorL0 for arbitrary integral even symmetric LatticeData with unit Gram determinant. For a in the full integer source-energy grade h, its raw t coefficient A_e satisfies [L0,A_e]=(e/2+h) A_e. There is no positivity, finite charge, finite grade dimension, symmetry, inversion or Jacobi premise.

The charged tensor seed supplies displacement (e+B(q,q))/2. A tensor-current commutator is added in the seed owner using its existing private inverse identities. Induction through both original normal-order branches gives each source jet weight r+1. Finite mode support is used only after applying to x and to L0 x; no finite endomorphism-valued sum is asserted.

Corr_coefficient_bidegree from the immutable repaired supplier gives s+sourceWeight(m)=R. Its exact original shift e+2s cancels s. The charge norm identity then gives e/2+chargeEnergy(q)+R. The existing carrier basis and grade span extend this law from monomials to every homogeneous source.

Source weight r+1 differs from the twisted oscillator odd weight 2r+1. The eigenvalue offset rank/16 is retained. The output integer index is M+e+2h, including negative values without conversion to Nat.

This is a classical algebraic twisted-Fock energy law, attributed to the FLM twisted lattice construction and the existing repository implementation; no literature novelty is asserted. It is a dependency for energy-restricted dual closure, not a completed VOA, CFT, string theory or AdS/CFT bridge.

The faithful mirrored Reg audit remains unfinished under the existing linked issue https://github.com/the-omega-institute/trureturing/issues/21259; kernel checking is separate from registration validation.

Theorem 1.1 (correctedField L zero commutator).

Lean statement: D5/S3/VertexAlgebra/HalfFock/ActualEnergyCovariance.correctedField_L_zero_commutator

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/HalfFock/ActualEnergyCovariance.correctedField_L_zero_commutator (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled theorem telescope supplies all parameters, hypotheses and the stated equality or vanishing law.

Theorem 1.2 (correctedField signed output).

Lean statement: D5/S3/VertexAlgebra/HalfFock/ActualEnergyCovariance.correctedField_signed_output

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/HalfFock/ActualEnergyCovariance.correctedField_signed_output (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled theorem telescope supplies all parameters, hypotheses and the stated equality or vanishing law.