Dinv
plain-language theorem explainer
Defines the inverse of the diagonal undeformed metric D = diag(cosh t_i) on R^n as the diagonal matrix with entries 1/cosh(t_i). Anyone working the general-n projector block reduction cites it as the concrete hInv kernel. The body is a one-line piecewise formula: inverse cosh on the diagonal, zero off-diagonal.
Claim. For ambient dimension $n$ and background $t \in \mathbb{R}^n$, the inverse undeformed metric is the diagonal kernel $(D^{-1}(t))_{ij} = \delta_{ij}/\cosh(t_i)$. Equivalently, $D^{-1}(t)$ is the matrix inverse of $D(t) = \mathrm{diag}(\cosh t_0,\ldots,\cosh t_{n-1})$, the Hessian of $\sum_i \cosh(t_i)$.
background
The module lifts 2D non-parallelism of the projector $P_\lambda$ to arbitrary ambient dimension $n$, for covectors $\alpha$ supported on two coordinates. The abstract projector is built as PApply from an inverse-metric kernel and a covector; the undeformed choice of kernel is this inverse diagonal metric.
Vectors are coordinate maps Vec n := Fin n → ℝ. The undeformed metric $D = \mathrm{diag}(\cosh t_i)$ is the Hessian of the uncoupled potential $\sum_i \cosh(t_i)$ (the $\lambda = 0$ part of $\Phi_\lambda$). Because $D$ is diagonal with strictly positive entries ($\cosh > 0$), its inverse is the diagonal of reciprocal coshes, written here as a bilinear kernel Fin n → Fin n → ℝ.
Module doc: instantiating the projector at this inverse metric and a 2-sparse $\alpha$, evaluated on the indicator direction $e_{i_0}$ with $t_{i_1} = 0$, collapses algebraically to the 2D closed form of the scalar certificates.
proof idea
Pure definition, no proof obligations. The body is the pointwise formula: on the diagonal return $(\cosh(t,i))^{-1}$; off-diagonal return $0$. Noncomputable only because it lands in ℝ with classical real inverse; no tactic script.
why it matters
This is the concrete $hInv$ that makes the general-$n$ block reduction run. Downstream, sharp_Dinv_apply shows the sharp map collapses to componentwise scaling by $1/\cosh(t_i)$; mu_Dinv_twoSparse reduces the scalar $\mu_\lambda$ to a two-term sum; and the block-reduction identity PApply_e_eq_P00Gen equates the $n$-dimensional projector entry to the 2D closed form P00Gen. From there PApply_not_parallel_gen transports the 2D non-vanishing derivative (Theorem 1a) to every ambient $n \ge 2$ on 2-sparse slices.
Curvature-bridge lemmas (dot_sharp_Dinv_twoSparse, hFull_mul_hInvFull) reuse the same kernel. In the Recognition cost geometry this is the flat, uncoupled background against which $\lambda$-deformations and non-parallelism of $P_\lambda$ are measured; it is scaffolding for the panel-requested general-$n$ architecture, not a forcing-chain landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.