Prove2Me

Closed form of the (B.3) series: 2∑bn=−ln⁡27162\sum b_n=-\ln\frac{27}{16}

Proved
ErlerGross.B3_series_closed_form

by Lucas · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsstring-field-theory
∑n≥1[22n−1−12n−23−12n−43]=−12ln⁡2716,\sum_{n\ge1}\left[\frac{2}{2n-1}-\frac{1}{2n-\frac23}-\frac{1}{2n-\frac43}\right]=-\frac12\ln\frac{27}{16},

i.e. the right side of (B.3) equals −ln⁡2716-\ln\frac{27}{16}.

Preamble
import Mathlib
import Definitions.Def_ErlerGross_defs
open Real Filter Topology MeasureTheory
Formal statement
namespace ErlerGross

theorem B3_series_closed_form :
    HasSum (fun n : ℕ => b3Term (n + 1)) (-Real.log (27 / 16) / 2) := 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), https://arxiv.org/abs/hep-th/0406199; Appendix B, p. 46 ('Writing eq. B.3 in terms of these summations, we find 3m2nβ2n=−ln⁡27163m_{2n}\beta_{2n}=-\ln\frac{27}{16}')
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, at the user's explicit request. It was not produced by a blind, independent auditor, and the author knew the intended meaning while writing it. Do not treat it as an independent audit; compare it against the Lean code and the source yourself.

The statement asserts that the real series ∑n≥1bn\sum_{n\ge1}b_n with

bn=22n−1−12n−23−12n−43b_n=\dfrac{2}{2n-1}-\dfrac{1}{2n-\frac23}-\dfrac{1}{2n-\frac43}

converges to −12ln⁡2716-\frac12\ln\frac{27}{16} (natural logarithm). "Converges to SS" means unconditional convergence of the real series (the net of finite partial sums tends to SS), which for real series is equivalent to absolute convergence with sum SS. No hypotheses.

Human review

  • Endorsed by Shuze Chen · Sep 26, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Sep 26, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph