dot_sharp_Dinv_twoSparse
plain-language theorem explainer
For a two-sparse vector α supported on distinct indices i0,i1, the quadratic form α · (D^{-1}♯ α) collapses to the two-term sum (cosh t_{i0})^{-1} α_{i0}^2 + (cosh t_{i1})^{-1} α_{i1}^2. Curvature-bridge authors cite it when reducing Shima sums on 2-sparse slices. Proof: componentwise diagonal identity, then the two-sparse sum lemma.
Claim. Let $n\in\mathbb{N}$, $t,\alpha\in\mathbb{R}^n$, and distinct indices $i_0,i_1\in\{0,\ldots,n-1\}$. If $\alpha$ vanishes off $\{i_0,i_1\}$, then $\sum_i \alpha_i\,(D(t)^{-1}\alpha)_i = (\cosh t_{i_0})^{-1}\alpha_{i_0}^2 + (\cosh t_{i_1})^{-1}\alpha_{i_1}^2$, where $D(t)=\mathrm{diag}(\cosh t_0,\ldots,\cosh t_{n-1})$.
background
The module lifts Theorem 2 (non-flatness of the deformed Hessian metric $h_\lambda$) from the 2D scalar certificates to arbitrary ambient dimension $n$. Metrics, inverses, third derivatives $\beta$, and Riemann components are bare arrays over $\mathrm{Fin},n$; curvature is Shima's formula $R_{ijkl}=\frac14\sum_{p,q}h^{pq}(\beta_{jkp}\beta_{ilq}-\beta_{ikp}\beta_{jlq})$.
$Dinv,t$ is the inverse of the undeformed diagonal Hessian $D=\mathrm{diag}(\cosh t_i)$ of $\sum_i\cosh t_i$. The sharp map applies a bilinear form as a matrix to a vector. Two-sparsity means $\alpha_k=0$ for all $k\notin{i_0,i_1}$, the general-$n$ stand-in for a pure 2D test vector.
Upstream, sharp_Dinv_apply gives $(D^{-1}\sharp\alpha)_i=(\cosh t_i)^{-1}\alpha_i$ for every $i$ (diagonal action). sum_twoSparse collapses any weighted sum $\sum_i f_i\alpha_i^2$ on a two-sparse $\alpha$ to the two support terms. The ordinary dot is $\sum_i\alpha_i t_i$.
proof idea
Pointwise identity first: for every index $i$, $\alpha_i\cdot(\mathrm{sharp}(Dinv,t),\alpha)_i=(\cosh t_i)^{-1}\alpha_i^2$, by rewriting with sharp_Dinv_apply and a one-line ring normalization.
Unfold dot to an explicit Finset sum, replace each summand by the pointwise identity via Finset.sum_congr, then invoke sum_twoSparse with weight $f(i)=(\cosh t_i)^{-1}$. Distinctness of $i_0,i_1$ and the two-sparsity hypothesis discharge the hypotheses of that lemma. No case splits on $n$ or on the values of $t$.
why it matters
Feeds the Stage B capstone RiemannMixedApply_reduce: under two-sparse $\alpha$ and $t_{i_1}=0$, the mixed component $R^{i_0}_{i_1,i_0,i_1}$ built from the genuine deformed $hFull$/$hInvFull$ and $\beta$ via Shima collapses algebraically to the certified negative closed form R0101Gen. That is the general-$n$ non-flatness content of the module.
The quadratic form $S=\alpha\cdot(D^{-1}\sharp\alpha)$ is the undeformed contribution that appears when the inverse metric contracts against $\beta$ factors. Restricting it to the two-sparse support is the first algebraic cut that lets every later spectator index drop out of the Shima sum. Without this identity the $n$-dimensional curvature arrays would not specialize to the 2D scalar certificate already proved negative in ScalarCertificates.
Architecturally it continues the bare-array, sum-manipulation strategy that closed Stage A (PApply_e_eq_P00Gen), avoiding abstract totally-geodesic arguments flagged dead by the panel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.