hInvFull_spectator
plain-language theorem explainer
On any spectator index k (α_k = 0, off the two-sparse support), every off-diagonal entry of the inverse deformed metric vanishes: (h_λ^{-1})_{kj} = 0 for j ≠ k. Curvature reductions that collapse the n-dimensional mixed Riemann component to the certified 2-D formula cite this vanishing to kill spectator summands. The proof unfolds the Sherman–Morrison inverse, uses diagonality of D^{-1}, and finishes by ring.
Claim. Let $\alpha,t\in\mathbb{R}^n$, $\lambda\in\mathbb{R}$, and indices $i_0,i_1,k,j\in\{0,\ldots,n-1\}$ satisfy $k\neq i_0$, $k\neq i_1$, $\alpha_k=0$, and $k\neq j$. Then the inverse of the deformed Hessian metric obeys $(h_\lambda^{-1})_{kj}=0$.
background
This module lifts Theorem 2 (non-flatness of the deformed Hessian metric $h_\lambda$) from the 2-D scalar certificates to arbitrary ambient dimension $n$. The undeformed diagonal metric is $D=\mathrm{diag}(\cosh t_0,\ldots,\cosh t_{n-1})$, the Hessian of $\sum_i\cosh t_i$; its inverse $D^{-1}$ is the matching diagonal of reciprocal coshes. The full deformed metric is the rank-one update $h_\lambda=D+\lambda\tilde g$, inverted in closed form by Sherman–Morrison as the bare array hInvFull.
A vector $\alpha$ is two-sparse on ${i_0,i_1}$ when every other coordinate vanishes. Spectator indices are those $k$ off that support, so $\alpha_k=0$. The mixed Riemann tensor is built from $h^{-1}$ and the third-derivative tensor $\beta$ via Shima's Hessian-curvature formula, implemented componentwise over $\mathrm{Fin},n$ with no manifold API.
Upstream, sharp_Dinv_apply records that $(D^{-1}\alpha)_i=(\cosh t_i)^{-1}\alpha_i$ for every $i$, by diagonality of $D^{-1}$. That identity is the only nontrivial input here.
proof idea
Unfold the Sherman–Morrison expression for the inverse deformed metric. The correction term is proportional to $w_k=(\cosh t_k)^{-1}\alpha_k$; rewrite that factor via sharp_Dinv_apply and substitute $\alpha_k=0$, so the whole rank-one correction vanishes at row $k$. What remains is the $(k,j)$ entry of the diagonal $D^{-1}$. Because $k\neq j$, the off-diagonal branch of $D^{-1}$ is zero (if_neg), and ring closes.
why it matters
Feeds the Stage B capstone RiemannMixedApply_reduce: under two-sparse $\alpha$ and $t_{i_1}=0$, the general-$n$ mixed component $R^{i_0}_{i_1,i_0,i_1}$ built from the actual deformed metric collapses algebraically to the closed form $R0101Gen$ already certified negative in the scalar certificates. Spectator vanishing is what lets every sum over ambient indices in Shima's formula restrict to the ${i_0,i_1}$ block, so the $n$-dimensional curvature construction genuinely specializes to the 2-D non-flatness certificate for arbitrary ambient $n$.
That specialization is the content of Theorem 2 in general dimension: the deformed Hessian metric is non-flat on every two-sparse slice. Architecturally it stays inside the panel-approved bare-array strategy (no totally-geodesic-submanifold argument). It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; those sit upstream of the cost potential whose Hessian is being curved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.