Lattices: theta series of an integral lattice

[CBirkbeck]

Goal

Define the theta series of an integral lattice L: the generating function counting vectors by norm,
Θ_L(z) = Σ_{v ∈ L} q^{½⟨v,v⟩} (q = e^{2πiz}), and prove it is a modular form on Γ₀(N) (an O(n)-link between lattices and modular forms).

What already exists

• mathlib: ZLattice, quadratic forms / BilinForm, ZLattice.covolume; modular forms API (ModularForm, q-expansions).
• Sibling repos SpherePacking8 / Sphere-Packing-Lean have lattice (E8/Leech) infrastructure to draw on.

What's missing

• thetaSeries L as a q-series counting r_L(n) = #{v ∈ L : ⟨v,v⟩ = 2n}, and (for even unimodular L) that it is a level-1 modular form of weight n/2.

Test cases

• Θ_{ℤ} = Jacobi θ₃; Θ_{E₈} = E₄ (weight 4, level 1); Θ_{ℤⁿ} = θ₃ⁿ.

LMFDB targets

• lattice.theta
• lattice.gram
• lattice.minimal_vector

New area, not yet in the Verso blueprint — links go to the LMFDB knowls.