sharp_Dinv_apply
plain-language theorem explainer
The inverse-metric raise of any covector α by the diagonal undeformed kernel Dinv(t) acts componentwise: the i-th entry is α_i / cosh(t_i). Anyone reducing n-dimensional projectors or curvature on 2-sparse slices cites this identity. The proof unfolds the definitions and collapses the defining sum to the single diagonal term via Finset.sum_eq_single.
Claim. For every ambient dimension $n$, background $t\in\mathbb{R}^n$, covector $\alpha\in\mathbb{R}^n$, and index $i$, the $i$-th component of the inverse-metric raise of $\alpha$ by the diagonal kernel $D^{-1}(t)=\mathrm{diag}(\cosh(t_0)^{-1},\ldots,\cosh(t_{n-1})^{-1})$ equals $\cosh(t_i)^{-1}\,\alpha_i$.
background
The module lifts 2D scalar certificates for the projector $P_\lambda$ to arbitrary ambient dimension $n$ on 2-sparse slices. The undeformed metric is the diagonal Hessian $D=\mathrm{diag}(\cosh(t_0),\ldots,\cosh(t_{n-1}))$ of the uncoupled potential $\sum_i\cosh(t_i)$; its inverse kernel is
$$D^{-1}(t)_{ij}=\begin{cases}\cosh(t_i)^{-1}&i=j\0&i\neq j.\end{cases}$$
The operator sharp raises a one-form $\beta$ by an inverse-metric kernel $h^{-1}$:
$$(h^{-1})^\sharp\beta,i=\sum_j h^{-1}{ij}\beta_j.$$
Vectors are coordinate maps $\mathrm{Fin},n\to\mathbb{R}$. Instantiating $h^{-1}:=D^{-1}(t)$ makes the sum diagonal, so each component factors. This holds for arbitrary $\alpha$, not only 2-sparse support; it is the general-$n$ algebraic fact that later collapses $\mu_\lambda$, $P_\lambda$, and mixed Riemann components on two-index slices.
proof idea
Term-mode proof. Unfold sharp and Dinv to expose the sum $\sum_j D^{-1}(t)_{ij}\alpha_j$. Apply Finset.sum_eq_single i: the matching term simplifies by the diagonal clause of Dinv to $\cosh(t_i)^{-1}\alpha_i$; every off-diagonal summand vanishes because $i\neq b$ forces the kernel entry to $0$; the missing-index branch is absurd since $i$ lies in Finset.univ. No external lemmas beyond the sum-singleton combinatorics and simp.
why it matters
This is the componentwise engine of the whole general-$n$ block reduction. Downstream, mu_Dinv_twoSparse rewrites each summand $\alpha_i\cdot(\mathrm{sharp},D^{-1}\alpha)i$ via this identity to obtain the two-term closed form for $\mu\lambda$; PApply_e_eq_P00Gen (the block-reduction identity equating the $n$-dimensional projector on $e_{i_0}$ to the 2D formula P00Gen) depends on the same collapse; and in CurvatureBridge, dot_sharp_Dinv_twoSparse, hInvFull_spectator, hFull_mul_hInvFull (Sherman–Morrison), and the Stage B capstone RiemannMixedApply_reduce all invoke it to show that abstract $n$-dimensional curvature specializes algebraically to the certified 2D non-flat form on any 2-sparse slice. In the Recognition cost geometry this underwrites the lift of Theorem 1a (non-parallelism of $P_\lambda$ w.r.t. the flat connection $D$) from $n=2$ to arbitrary $n$, without approximation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.