mu_Dinv_twoSparse
plain-language theorem explainer
For any ambient dimension n, the projector scalar μ_λ built from the inverse undeformed metric Dinv(t) and a covector α supported on exactly two indices collapses to a two-term closed form: λ times the sum of (cosh t_i)^{-1} α_i² on those two slots. Anyone proving the general-n block reduction of P_λ to the 2D certificate P00Gen cites this. The proof unfolds μ, applies the diagonal action of Dinv, then collapses the sum by 2-sparsity.
Claim. Let $n\in\mathbb{N}$, $t,\alpha\in\mathbb{R}^n$, $\lambda\in\mathbb{R}$, and distinct indices $i_0,i_1$. If $\alpha$ vanishes off $\{i_0,i_1\}$, then the projector scalar $\mu_\lambda$ evaluated at the inverse undeformed metric $D^{-1}(t)$ and at $\alpha$ equals $\lambda\bigl((\cosh t_{i_0})^{-1}\alpha_{i_0}^2+(\cosh t_{i_1})^{-1}\alpha_{i_1}^2\bigr)$.
background
This module lifts the 2D non-parallelism certificates for the projector $P_\lambda$ to arbitrary ambient dimension $n$, on any covector $\alpha$ supported on two coordinates (a "2-sparse" slice). The undeformed metric is the diagonal $D=\mathrm{diag}(\cosh t_0,\ldots,\cosh t_{n-1})$, the Hessian of $\sum_i\cosh t_i$; its inverse $D^{-1}(t)$ is the diagonal kernel with entries $(\cosh t_i)^{-1}$.
The scalar $\mu_\lambda(h^{-1},\alpha)$ is the normalization factor inside the abstract projector $P_\lambda=P\mathrm{Apply}(\lambda,h^{-1},\alpha)$ from Projector.lean: essentially $\lambda$ times the pairing of $\alpha$ against the raised covector $\sharp(h^{-1})\alpha$. TwoSparse $\alpha,i_0,i_1$ means $\alpha_k=0$ for all $k\notin{i_0,i_1}$, the general-$n$ stand-in for the 2D setup $\alpha=(a,b)$.
Upstream, sharp_Dinv_apply records that $\sharp(D^{-1}t)\alpha$ is componentwise $(\cosh t_i)^{-1}\alpha_i$ for every $\alpha$, and sum_twoSparse collapses any weighted sum $\sum_i f_i\alpha_i^2$ over a 2-sparse $\alpha$ to the two surviving terms.
proof idea
Unfold $\mu$. First prove the pointwise identity $\alpha_i\cdot(\sharp(D^{-1}t)\alpha)_i=(\cosh t_i)^{-1}\alpha_i^2$ for every coordinate $i$, by rewriting with sharp_Dinv_apply and simplifying. The Euclidean pairing $\mathrm{dot}(\alpha,\sharp(D^{-1}t)\alpha)$ is then exactly $\sum_i(\cosh t_i)^{-1}\alpha_i^2$ by congruence of the finite sum. Finally apply sum_twoSparse with weight $f(i)=(\cosh t_i)^{-1}$ to drop every term outside ${i_0,i_1}$, leaving the claimed two-term formula multiplied by $\lambda$.
why it matters
This is the scalar half of the algebraic block reduction that makes Theorem 1a (non-parallelism of $P_\lambda$ w.r.t. the flat connection) hold in every ambient dimension, not merely $n=2$. Downstream, PApply_e_eq_P00Gen uses it to show that the $(i_0,i_0)$ entry of the genuinely $n$-dimensional projector $P\mathrm{Apply}(\lambda,D^{-1}t,\alpha)$ applied to the indicator $e_{i_0}$ equals exactly the 2D closed form $P00\mathrm{Gen}(\alpha_{i_0},\alpha_{i_1},t_{i_0})$ of ScalarCertificates, under $t_{i_1}=0$, $\alpha_{i_0}\neq 0$, $\lambda\neq 0$.
Because the two sides agree as functions of the free coordinate, the already-proved 2D derivative certificate $dP00\mathrm{Gen}\neq 0$ transports verbatim to the general-$n$ non-parallelism statement PApply_not_parallel_gen. The reduction is equality of reals computed from the $n$-dimensional definitions, not an isomorphism or numerical check. In the broader Recognition cost geometry this is the Christoffel/projector-component block-diagonalization on 2-sparse slices that the review panel required for the general-$n$ architecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.