Mode series equals twice the B.3 scalar series

Proved

ErlerGross.mode_sum_eq_B3_identity

by Eyal1990 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsstring-field-theory

The mode series in Erler–Gross Eq. (B.3) has sum twice the scalar series displayed there:

\sum_{n\ge 1}3m_{2n}\beta_{2n}=2\sum_{n\ge 1}\left(\frac{2}{2n-1}-\frac{1}{2n-\frac23}-\frac{1}{2n-\frac43}\right).

In the Lean indexing, both sums start at index +1 $for \in\mathbb N$ . The scalar-series summand is ErlerGross.b3Term; the mode summand uses eumannMEven and etaVec. This is the identity component of the formalized Eq. (B.3).

Preamble

import Definitions.Def_ErlerGross_defs
open Real Filter Topology MeasureTheory
open ErlerGross

Formal statement

namespace ErlerGross
theorem mode_sum_eq_B3_identity :
    HasSum (fun n : ℕ => 3 * neumannMEven (n + 1) * betaVec (2 * (n + 1)))
      (2 * ∑' n : ℕ, b3Term (n + 1)) := by
  sorry
end ErlerGross

Source

T. G. Erler and D. J. Gross, Locality, Causality, and an Initial Value Formulation for Open String Field Theory, arXiv:hep-th/0406199v2 (2004), Appendix B, eq. (B.3), p. 46

View graph