Motivation

In Witten's cubic open string field theory (Witten 1986) the interaction glues half-strings together, and in the usual center-of-mass variables the action contains infinitely many time derivatives. Such a theory has no evident initial value formulation, which obstructs a Hamiltonian treatment and a direct discussion of causality.

Erler and Gross (2004) show that after a unitary change of basis in which the string field depends on the lightcone component of the string midpoint $x^+(\pi/2)$ (and on transverse center-of-mass coordinates), the cubic vertex contains no derivatives with respect to lightcone time. This reduces to five linear relations among the Neumann coefficients of the three-string vertex, the midpoint identities (A.6)–(A.10) of the paper. One of them, (A.8), is a closed numerical identity: a specific infinite series built from Neumann coefficients equals $-\ln\frac{27}{16}$, where $\ln\frac{27}{16}=V_{00}$ is the zero-mode Neumann coefficient. This mission formalizes that identity and the chain of intermediate results the paper uses to prove it (Appendix B), together with a divergence statement from Section 2 explaining why other midpoint bases fail.

Setting

Define real constants $A_k$ ($k\ge0$) by the expansion

$$\left(\frac{1+iz}{1-iz}\right)^{1/3}=\exp\!\left(\tfrac{2i}{3}\tan^{-1}z\right)=1+\sum_{n\ge1}A_{2n}z^{2n}+i\sum_{n\ge1}A_{2n-1}z^{2n-1}.$$

For real $z$ the left side is $\cos(\tfrac23\arctan z)+i\sin(\tfrac23\arctan z)$, so $A_{2n}$ is the $2n$-th Taylor coefficient of $\cos(\tfrac23\arctan z)$ at $0$ (e.g. $A_2=-\tfrac29$). The even Neumann vector and the vector $\beta$ are

$$m_{2n}=-\frac23\,\frac{A_{2n}}{\sqrt{2n}},\qquad \beta_k=\frac{\cos(k\pi/2)}{\sqrt k},\quad\text{so }\beta_{2n}=\frac{(-1)^n}{\sqrt{2n}}.$$

In Lean these are ErlerGross.neumannA, ErlerGross.neumannMEven (with neumannMEven n $=m_{2n}$) and ErlerGross.betaVec. Two auxiliary objects appear in the proof: the (B.3) terms

$$b_n=\frac{2}{2n-1}-\frac{1}{2n-\frac23}-\frac{1}{2n-\frac43}\qquad(n\ge1),$$

(ErlerGross.b3Term) and the $\kappa$-basis integrand

$$g(\kappa)=\frac{1-\cosh\frac{\pi\kappa}{2}}{1+2\cosh\frac{\pi\kappa}{2}}\cdot\frac{1}{2\kappa\sinh\frac{\pi\kappa}{2}}$$

(ErlerGross.kappaIntegrand), which arises from the continuous spectrum $\kappa\in\mathbb R$ of the Neumann matrices (Rastelli–Sen–Zwiebach 2001).

Formalization targets

Goal — midpoint identity (A.8)

$$\ln\frac{27}{16}+\sum_{n\ge1}3\,m_{2n}\beta_{2n}=0,$$

formalized as: the series $\sum_{n\ge1}3m_{2n}\beta_{2n}$ converges absolutely (Lean HasSum) to $-\ln\frac{27}{16}$.

Milestones (Appendix B and Section 2)

• $\kappa$-basis representation: $g$ is integrable and $\sum_{n\ge1}3m_{2n}\beta_{2n}=2\int_{\mathbb R}g$.
• Residue evaluation: $\int_{\mathbb R}g=\sum_{n\ge1}b_n$.
• Eq. (B.3): $\sum_{n\ge1}3m_{2n}\beta_{2n}=2\sum_{n\ge1}b_n$.
• Auxiliary series: $\sum_{n\ge1}\frac{1}{n(2n+1)}=2-2\ln2$ and $\sum_{n\ge1}\frac{1}{n(9n^2-1)}=\frac32(\ln3-1)$.
• Closed form: $\sum_{n\ge1}b_n=-\frac12\ln\frac{27}{16}$.
• Integral formula: $\int_0^\infty\frac{\cosh ax}{\cosh bx}\,dx=\frac{\pi}{2b}\frac{1}{\cos\frac{\pi a}{2b}}$ for complex $a,b$ with $|\Re a|<\Re b$.
• Section 2: for any real regulator with $\omega_{2n}\to0$, $\sum_{n\ge1}\frac{((-1)^n-\omega_{2n})^2}{2n}=+\infty$.

Significance

In the paper, (A.8) is one of the relations which, together with (A.6), (A.7), (A.9), (A.10), removes lightcone-time derivatives from the cubic vertex. This is what gives the theory an initial value formulation in lightcone time and makes the Hamiltonian BRST quantization of Section 4 possible. Unlike the other four identities, which are relations between distributions and are verified in the paper's spectral basis, (A.8) is an equality of real numbers. It can therefore be checked completely in Lean.

A complete formalization would produce a machine-checked proof of a Neumann-coefficient identity. It would also add reusable material: Taylor coefficients of $\exp(\tfrac{2i}{3}\arctan z)$, the $\cosh/\cosh$ integral, and digamma-type evaluations of rational series.

Difficulty

The goal defines $m_{2n}$ through Taylor coefficients, which have no closed form. The paper does not sum the series in the mode basis. It moves to the continuous $\kappa$ basis of the Neumann spectrum and closes a contour. That step rests on eigenvector expansions $v_{2n}(\kappa)$ and the principal-value distribution $\beta(\kappa)$, neither of which is in Mathlib. A direct route has to connect the coefficients $A_{2n}$ to the integral $\int g$, or to the series $\sum b_n$, some other way. The terms of $\sum b_n$ decay like $n^{-2}$. The terms $(-1)^nA_{2n}/n$ of the goal series decay only like $n^{-5/3}$, so the goal series converges slowly.

Formalization scope

• All quantities are real. $A_k$ is given as $f^{(k)}(0)/k!$ for $f=\cos(\tfrac23\arctan\cdot)$ (even $k$) or $\sin(\tfrac23\arctan\cdot)$ (odd $k$), using Mathlib's iteratedDeriv.
• Series are indexed from $n=1$ by shifting the Lean index $n\mapsto n+1$. HasSum is unconditional (equivalently absolute) convergence. Every statement asserts convergence, so no statement can hold only because Lean assigns $0$ to a divergent tsum.
• $g(0)=0$ by Lean's convention $x/0=0$. This single point does not affect the integral.
• Source misprints corrected: the paper's first auxiliary formula prints $\sum\frac{1}{n(2n+1)}=2-\ln2$. The true value is $2-2\ln2\approx0.6137$, and that value is formalized. The formula for $m_{2n}$ is printed with left side $m_{2m}$.
• In the Section 2 statement the dimension factor $D>0$ is omitted, and only divergence to $+\infty$ is asserted, not the logarithmic rate.
• Not formalized: the identities (A.6), (A.7), (A.9), (A.10), eq. (B.2), and the eigenvectors $v_n(\kappa)$. Contributions that build this spectral machinery are welcome.

Selected references

• T. G. Erler, D. J. Gross, Locality, Causality, and an Initial Value Formulation for Open String Field Theory, 2004. https://arxiv.org/abs/hep-th/0406199
• E. Witten, Noncommutative Geometry and String Field Theory, Nucl. Phys. B 268 (1986) 253. https://doi.org/10.1016/0550-3213(86)90155-0
• L. Rastelli, A. Sen, B. Zwiebach, Star Algebra Spectroscopy, JHEP 2002. https://arxiv.org/abs/hep-th/0111281