Theta Grade Trace Split
Abstract
The theta trace on each finite energy grade is the fixed-minus-anti-fixed dimension.
For a positive-definite lattice datum D and an integer energy grade n, grade D n is finite-dimensional. Its theta-even part is grade D n intersect fixedSpace D, and its theta-odd part is grade D n intersect minusSpace D.
Theorem 1.1 (Twined trace splits by theta eigenspaces).
Lean statement: D5/S3/VertexAlgebra/SourceBPZ/ThetaGradeTraceSplit.grade_theta_trace_eq_fixed_minus_anti
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/SourceBPZ/ThetaGradeTraceSplit.grade_theta_trace_eq_fixed_minus_anti (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every positive-definite D and integer n, the trace of theta on grade D n equals the complex dimension of its theta-fixed submodule minus the complex dimension of its theta-anti-fixed submodule.