Pith. sign in
theorem

riemann_beta_numerator_zero

proved
show as:
module
IndisputableMonolith.Cost.Ndim.CurvatureBridge
domain
Cost
line
235 · github
papers citing
none yet

plain-language theorem explainer

When α is two-sparse on {i0,i1} and at least one of the free indices p,q lies off that support, the Shima numerator β_{i1 i0 p} β_{m i1 q} − β_{m i0 p} β_{i1 i1 q} vanishes for every m. Curvature-bridge authors cite it to kill spectator summands in the general-n Riemann component. Proof: case-split on the spectator, invoke β-vanishing, then ring.

Claim. Let $\alpha,t\in\mathbb{R}^n$, $\lambda\in\mathbb{R}$, and $i_0\neq i_1$. Suppose $\alpha$ is supported on $\{i_0,i_1\}$. For any $m,p,q\in\{0,\ldots,n-1\}$, if $p\notin\{i_0,i_1\}$ or $q\notin\{i_0,i_1\}$, then $\beta(\alpha,t,\lambda)_{i_1 i_0 p}\,\beta(\alpha,t,\lambda)_{m i_1 q}-\beta(\alpha,t,\lambda)_{m i_0 p}\,\beta(\alpha,t,\lambda)_{i_1 i_1 q}=0$, where $\beta_{ijk}=\partial_i\partial_j\partial_k\Phi_\lambda$ is the third-derivative tensor of the deformed potential.

background

This module lifts Theorem 2 (non-flatness of the deformed Hessian metric $h_\lambda$) from the 2-D certificates to arbitrary ambient dimension $n$. The metric is the bare array $h_\lambda=D+\lambda\tilde g$, inverted by Sherman–Morrison; curvature is built from 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_\lambda$.

The potential is $\Phi_\lambda(t)=\sum_i\cosh(t_i)+\lambda(\cosh(\alpha\cdot t)-1)$, so $\beta$ has the closed form $\beta_{ijk}=(\text{if }i=j=k\text{ then }\sinh(t_i)\text{ else }0)+\lambda,\alpha_i\alpha_j\alpha_k\sinh(\alpha\cdot t)$. TwoSparse means $\alpha_k=0$ for all $k\notin{i_0,i_1}$ — the general-$n$ analogue of the 2-D setup. The upstream lemma beta_eq_zero records that any zero $\alpha$-slot kills $\beta$ whenever the pure diagonal term does not fire; that is the structural engine of the block collapse.

proof idea

Case-split on the spectator hypothesis. If $p$ is off support, TwoSparse forces $\alpha_p=0$. Apply beta_eq_zero twice: once to $\beta_{i_1 i_0 p}$ (the diagonal clause fails because $i_1\neq i_0$) and once to $\beta_{m i_0 p}$ (diagonal fails because $p\neq i_0$). Both factors vanish, so the difference is zero by ring. The $q$-off-support branch is symmetric: $\alpha_q=0$ kills $\beta_{m i_1 q}$ and $\beta_{i_1 i_1 q}$ (the latter because $q\neq i_1$), and again ring finishes. No metric inverse or sum identity is needed — pure $\beta$-vanishing.

why it matters

This is the core vanishing fact that drives the Stage B capstone. Downstream, RiemannMixedApply_reduce uses it to show that under TwoSparse $\alpha$ and $t_{i_1}=0$, the mixed component $R^{i_0}_{i_1 i_0 i_1}$ built from the genuine $n$-dimensional $h$/$h^{-1}$ and $\beta$ via Shima collapses algebraically to the closed form R0101Gen already certified negative in ScalarCertificates. That is the general-$n$ non-flatness content: the abstract curvature construction specializes to the certified 2-D formula on every 2-sparse slice, for arbitrary ambient $n$. Architecturally it follows the panel-greenlit bare-array strategy (no manifold API), matching the Stage A projector reduction. It does not itself touch T0–T8 or the RCL; it is pure cost-geometry scaffolding for the Hessian non-flatness theorem.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.