beta_eq_zero
plain-language theorem explainer
The third-derivative tensor β_ijk of the deformed potential vanishes whenever any index carries a zero α-component and the three indices are not all equal. Anyone collapsing Shima's Riemann sum under TwoSparse support cites this. The proof unfolds the closed form, kills the diagonal sinh branch by the inequality hypothesis, then cases on which α vanishes and simplifies by ring.
Claim. Let $\alpha,t\in\mathbb{R}^n$, $\lambda\in\mathbb{R}$, and $i,j,k\in\{0,\ldots,n-1\}$. Write $\beta_{ijk}=\partial_i\partial_j\partial_k\Phi_\lambda$ for the third derivatives of $\Phi_\lambda(t)=\sum_r\cosh(t_r)+\lambda(\cosh(\alpha\cdot t)-1)$. If $\alpha_i=0$ or $\alpha_j=0$ or $\alpha_k=0$, and it is not the case that $i=j=k$, then $\beta_{ijk}=0$.
background
This module lifts Theorem 2 (non-flatness of the deformed Hessian metric $h_\lambda$) to ambient dimension $n$. It builds the bare-array metric $h_\lambda=D+\lambda\tilde g$, its Sherman-Morrison inverse, the third-derivative tensor $\beta$, and the Riemann tensor via Shima's formula for Hessian structures:
$R_{ijkl}=\frac14\sum_{p,q}h^{pq}(\beta_{jkp}\beta_{ilq}-\beta_{ikp}\beta_{jlq})$, with $\beta_{ijk}=\partial_i\partial_j\partial_k\Phi$.
Here $\mathrm{Vec},n:=\mathrm{Fin},n\to\mathbb{R}$ is the bare coordinate type. The tensor $\beta$ is defined in closed form as the diagonal piece $\sinh(t_i)$ when $i=j=k$, plus the rank-one deformation $\lambda,\alpha_i\alpha_j\alpha_k\sinh(\alpha\cdot t)$. A spectator index is one with $\alpha_s=0$ (off the TwoSparse support of $\alpha$). The present lemma records that any such spectator kills every off-diagonal $\beta$ entry that touches it.
proof idea
Unfold the closed-form definition of $\beta$. The hypothesis $\neg(i=j\land j=k)$ forces the diagonal branch to the zero arm via if_neg, leaving only the product term $\lambda,\alpha_i\alpha_j\alpha_k\sinh(\alpha\cdot t)$. Case-split on which of $\alpha_i,\alpha_j,\alpha_k$ vanishes; rewrite that factor to zero and finish by ring. No external lemmas are required beyond the definition.
why it matters
This is the elementary vanishing engine behind the block-diagonal collapse of Shima's $(p,q)$-sum. Downstream, riemann_beta_numerator_zero applies it repeatedly: for $p$ or $q$ off the TwoSparse support, every $\beta$-factor in the numerator at the mixed indices $(i_1,i_0,\cdot)$, $(m,i_0,\cdot)$, $(m,i_1,\cdot)$, $(i_1,i_1,\cdot)$ is zero, so the whole summand dies. That reduction is what lets the mixed Riemann component $R^{i_0}{}{i_1,i_0,i_1}$ collapse to the certified negative closed form already proved in ScalarCertificates, completing the $n$-dimensional non-flatness statement for $h\lambda$. In the broader Recognition cost geometry this is Stage-B infrastructure: bare-array curvature identities, not abstract totally-geodesic restriction arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.