A Bernoulli–harmonic–zeta identity for the free scalar on hyperbolic space

T. Nishioka and Y. Sato (arXiv:2101.02399, hep-th; JHEP 05 (2021) 074) compute the free energy of a conformally coupled free scalar on hyperbolic space. In the derivative of the spectral zeta function for even dimension they need, for every k ≥ 0,

`−2^{−2k−2}/(k+1) H_{2k+1} − Σ_{m=1}^{k} 2^{−2k−2}(2^{2m}−2)/(k−m+1) · B_{2m}/(2m)

• Σ_{j=0}^{2k+1} (−1)^j/2^{2k−j} · C(2k+1, j) H_j ζ(−j) + (1 − 2^{−2k−1}) H_{2k+1} B_{2k+2}/(k+1) = 0`

(eq. (C.12) of the published text), and state: "We confirmed (C.12) up to k = 100 numerically. However, we do not know a proof of (C.12)." Issue #11322 fixes the reading: H_j the harmonic numbers, B_n the Bernoulli numbers with B_1 = −1/2, ζ the Riemann zeta function.

The identity removes all terms other than ζ'(−j) from ∂_s ζ_{H^d}(0, 1/2), which the paper uses for the free energy on H^d and its defect C-theorem. The follow-up on the free fermion (arXiv:2102.11468) records that the scalar case was checked only numerically. The frozen declaration D5/S3/Quantum/FockSpace/HyperbolicScalarZetaIdentity.result proves the identity for every k; the physical consequence is not formalized.

Issue #11322 preregisters the reading, the route and the literature check. arXiv v5 and the published JHEP text state the identity without proof. INSPIRE lists 38 citing records; the 34 arXiv full texts were searched and none proves or restates it. Boyadzhiev (arXiv:1701.00544) evaluates Σ C(n, k) H_k B_k, a different sum.

These readings are not-found-in-searched-scope; they do not establish an exhaustive worldwide literature search, priority, or the absence of an independent answer.

Put N = 2k + 2 and b_m = Σ_i C(m, i) 2^i B_i.

1. b_m = 2^m B_m(1/2) = (2 − 2^m) B_m by the value of the Bernoulli polynomial at 1/2 (Mathlib's bernoulliFun_eval_half); in particular b_m = 0 for odd m.
2. With ζ(−j) = (−1)^j B_{j+1}/(j+1) and after multiplying by 2^N (k+1), the middle sum is Σ_{1≤i≤N−1} b_i (1/i + 1/(N−i)) and the zeta sum is Σ_{1≤i≤N} C(N, i) 2^i B_i H_{i−1}.
3. C(n, i)(H_n − H_i) = Σ_{j=1}^{n} C(n−j, i)/j and Σ_i C(n, i) 2^i B_i / i = Σ_{j=1}^{n} (b_j − 1)/j turn the zeta sum into sums of b_i/i and b_{N−i}/i, which cancel against the middle sum; what is left is −H_{N−1} − 1/N + H_N = 0.

The answer would change if B_1 were taken as +1/2 or ζ(0) differed from −1/2; or if H_j were shifted: replacing H_j by H_{j+1} gives −5/12 at k = 0.

Exact rational arithmetic (issue #11322): the left side is 0 for k = 0, …, 60. Dropping 2^{−2k−1} from the last coefficient gives 1/12, −11/2880, …, and no zero for k ≤ 20.

The canonical source is D5/S3/Quantum/FockSpace/HyperbolicScalarZetaIdentity.lean. Its public declarations are claim and result. The frozen module state has statement identity sha256:13a21460fdd4da0d876280b4e0f84827b2d98c97b0be77795f0d5d5a9008ec0b. The result declaration has statement identity sha256:fc7f2aa577e096bb0f6203e18e5592dcdc8f994af0f4e8cdca30688a856ea95c. The Freeze event is sha256:1cb4a9a2fe4e397bd01733f9ff42f200f41e199960e0b6d0743f11386d008f81 and has no project-level frozen prerequisites. The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Tier 1 external named conjecture, preregistered in issue #11322 before any Lean. theorem; resolution proved. The public theorem has proof_shape: content: the harmonic–binomial identities and the telescoping are proved in the module, and the value of the Bernoulli polynomials at 1/2 is taken from Mathlib. Its escape witness is form (1), and its admission basis is open-problem-resolution. Utility none: the identity is proved for every k.

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent answer. The Lean kernel does not authenticate the external source or its version history.