hInvFull
plain-language theorem explainer
Defines the coordinate inverse of the deformed Hessian metric h_λ = D + (λc) α⊗α via the Sherman-Morrison formula: D⁻¹ minus a rank-one correction built from D⁻¹α. Anyone proving two-sided invertibility of h_λ or evaluating Shima curvature components in ambient dimension n cites this array. The body is the classical SM formula written componentwise; no proof obligations.
Claim. For vectors $\alpha,t\in\mathbb{R}^n$ and scalar $\lambda\in\mathbb{R}$, the inverse kernel of the deformed metric is the array $$h^{-1}_{ij}=D^{-1}_{ij}-\frac{\lambda c}{1+\lambda c\,S}\,(D^{-1}\alpha)_i(D^{-1}\alpha)_j,$$ where $D=\mathrm{diag}(\cosh t_k)$, $c=\cosh(\alpha\cdot t)$, $S=\alpha\cdot(D^{-1}\alpha)$, and $D^{-1}\alpha$ is the index-raised vector.
background
This module lifts Theorem 2 (non-flatness of the deformed Hessian metric $h_\lambda$) from the 2D scalar certificates to arbitrary ambient dimension $n$. The undeformed background is the diagonal Hessian $D=\mathrm{diag}(\cosh t_i)$ of $\sum_i\cosh t_i$; its inverse $D^{-1}$ is the pointwise reciprocal on the diagonal and zero off it.
The deformation is the rank-one update $h_\lambda=D+(\lambda c),\alpha\otimes\alpha$ with $c=\cosh(\alpha\cdot t)$. The weighted dot $\alpha\cdot t=\sum_i\alpha_i t_i$ is the logarithmic aggregate from the $n$-dimensional cost core. Raising a covector by a kernel $h^{-1}$ is the contraction $(\sharp_{h^{-1}}\beta)i=\sum_j h^{-1}{ij}\beta_j$.
Sherman-Morrison supplies the exact inverse of a rank-one update of an invertible matrix whenever the scalar denominator $1+\lambda c,S$ is nonzero, with self-energy $S=\alpha\cdot(D^{-1}\alpha)$. The construction is bare arrays over $\mathrm{Fin},n$: no Matrix API, matching the panel architecture used for the projector non-parallelism theorem.
proof idea
Pure definition: the body is the classical Sherman-Morrison formula written componentwise. The diagonal piece is $D^{-1}{ij}$. The correction coefficient is $\lambda c/(1+\lambda c,S)$ with $c=\cosh(\alpha\cdot t)$ and $S=\alpha\cdot(\sharp{D^{-1}}\alpha)$. The outer product is assembled from the raised vector $\sharp_{D^{-1}}\alpha$ evaluated at the two free indices $i,j$. No tactics, no lemmas applied at the definition site.
why it matters
This inverse is the $n$-dimensional bridge from the deformed metric into Shima's curvature formula. Downstream, hFull_mul_hInvFull proves it is genuinely the two-sided inverse for any $n$ (no TwoSparse hypothesis), which is the module's main algebraic content. Symmetry, spectator vanishing off the TwoSparse support, and the mixed Riemann applicator all consume this array.
The Stage B capstone RiemannMixedApply_reduce feeds $h^{-1}$ and the third-derivative tensor $\beta$ into Shima's sum and collapses $R^{i_0}{i_1,i_0,i_1}$ to the certified 2D closed form $R{0101}^{\mathrm{Gen}}$. Negativity of that component (RiemannMixedApply_neg) is Theorem 2 in general $n$: $h_\lambda$ is non-flat for any ambient dimension whenever $\alpha$ is two-sparse. Without an explicit inverse kernel, the bare-array curvature construction cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.