A Proof of the Purely Arithmetic Characterization of Linear Relations among Theta Series of Quadratic Lattices

A Proof of the Purely Arithmetic Characterization of Linear Relations among Theta Series of Quadratic Lattices, with Complete Lean 4 Formalization Let \(V\) be a positive-definite quadratic space over \(\mathbb{Q}\), and fix an order \(\mathcal O\) of full \(\mathbb{Z}\)-lattices in \(V\), where lattices belong to the same order when their normalized Gram matrices have the same elementary divisors over \(\mathbb{Z}_p\) for every prime \(p\). Let \(L_1,\ldots,L_h\) represent the rational-similarity classes in \(\mathcal O\), and let \(Q_i\) be the associated normalized integral quadratic form on \(L_i\). Define the formal theta series \[ \theta_{L_i}(q) =\sum_{x\in L_i}q^{Q_i(x)} =\sum_{m\ge 0}r_{L_i}(m)q^m \in\mathbb{Z}[[q]] \] and the theta map \[ \Theta_{\mathcal O}:\mathbb{C}^{h}\longrightarrow\mathbb{C}[[q]], \qquad (c_1,\ldots,c_h)\longmapsto \sum_{i=1}^{h}c_i\theta_{L_i}(q). \] We prove the stated arithmetic characterization and provide a complete Lean 4 formalization of the resulting mathematical development. Our construction determines all complex linear relations among the complete formal theta series, constructs a linearly independent basis for their image, and expresses every input theta series uniquely in that basis. The proof uses the arithmetic of quadratic lattices, exact algebra, formal \(q\)-series, and algebraic constructions of modular forms, without relying on analytic theta transformations, Poisson summation, or analytic valence formulas.