PApply_e_eq_P00Gen
plain-language theorem explainer
On any ambient dimension n, a 2-sparse covector α supported on i0≠i1, and a background t with t_{i1}=0, the (i0,i0) entry of the n-dimensional projector P_λ applied to the indicator e_{i0} equals exactly the 2D closed form P00Gen(α_{i0},α_{i1},t_{i0}). Anyone lifting non-parallelism of P_λ from n=2 to general n cites this identity. The proof collapses the abstract projector sums via diagonality of Dinv and two-sparsity, then matches the scalar formula by field arithmetic.
Claim. Let $n\ge 2$, $t,\alpha\in\mathbb{R}^n$, $\lambda\in\mathbb{R}$, and $i_0\ne i_1$. Suppose $\alpha$ vanishes off $\{i_0,i_1\}$, $\alpha_{i_0}\ne 0$, $\lambda\ne 0$, and $t_{i_1}=0$. Then the $(i_0,i_0)$ entry of the abstract projector $P_\lambda$ built from the inverse undeformed metric $D(t)^{-1}$ and covector $\alpha$, evaluated on the indicator direction $e_{i_0}$, equals the 2D scalar closed form $P_{00}^{\mathrm{Gen}}(\alpha_{i_0},\alpha_{i_1},t_{i_0})$.
background
The module lifts Theorem 1a (non-parallelism of the projector $P_\lambda$ w.r.t. the flat connection $D$) from ambient dimension $n=2$ to arbitrary $n$. In Projector.lean, $P_\lambda$ is the abstract operator-algebra projector PApply built from an inverse-metric kernel $h^{-1}$ and a covector $\beta$. Instantiating $h^{-1}:=D^{-1}(t)$, the inverse of the diagonal undeformed metric $D=\mathrm{diag}(\cosh t_0,\ldots,\cosh t_{n-1})$ (Hessian of $\sum_i\cosh t_i$), and $\beta:=\alpha$ 2-sparse on $i_0\ne i_1$, the general-$n$ sums defining the projector are expected to collapse to a 2D formula.
Two-sparsity means $\alpha_k=0$ for all $k\notin{i_0,i_1}$. The indicator $e_{i_0}$ extracts the $(i_0,i_0)$ matrix entry. Upstream, sharp_Dinv_apply records that $D^{-1}(t)$ is diagonal, so $\sharp(D^{-1}t),\alpha$ at index $i$ is just $(\cosh t_i)^{-1}\alpha_i$; mu_Dinv_twoSparse collapses the scalar $\mu_\lambda$ to the two-term form $\lambda\bigl((\cosh t_{i_0})^{-1}\alpha_{i_0}^2+(\cosh t_{i_1})^{-1}\alpha_{i_1}^2\bigr)$; and dot_e gives $\langle\alpha,e_{i_0}\rangle=\alpha_{i_0}$. The 2D closed form $P_{00}^{\mathrm{Gen}}$ lives in ScalarCertificates.lean.
proof idea
Positivity lemmas first: $\cosh(t_{i_0})>0$ and $\alpha_{i_0}^2>0$. The numerator side uses sharp_Dinv_apply and dot_e to rewrite $A_\lambda(D^{-1}t,\alpha)(e_{i_0}){i_0}$ as $\lambda\cdot(\cosh t{i_0})^{-1}\alpha_{i_0}\cdot\alpha_{i_0}$. The denominator side applies mu_Dinv_twoSparse, substitutes $t_{i_1}=0$ (so $\cosh 0=1$), and obtains $\mu=\lambda\bigl((\cosh t_{i_0})^{-1}\alpha_{i_0}^2+\alpha_{i_1}^2\bigr)$. Two nlinarith steps confirm the relevant denominators are strictly positive. Unfolding the definition of PApply as $\mu^{-1}\cdot A$, substituting both closed forms, unfolding $P_{00}^{\mathrm{Gen}}$, and clearing the common positive denominator by field_simp yields the equality.
why it matters
This is the algebraic content of the panel-greenlit general-$n$ architecture: the genuinely $n$-dimensional projector is not merely isomorphic to, or expected to reduce to, the 2D closed form on a 2-sparse slice; the two sides are equal as real numbers. Downstream, PApply_not_parallel_gen (Theorem 1a for arbitrary $n$) transports the already-proved 2D derivative nonvanishing dP00Gen_ne_zero along this identity: because both sides agree as functions of the free coordinate $t_{i_0}$, they share derivatives, so $P_\lambda$ fails to be $D$-parallel along $e_{i_0}$ at every point of the slice, for every $n\ge 2$.
In the Recognition cost geometry, $D$ is the undeformed Hessian block of the potential $\Phi_\lambda$; non-parallelism of $P_\lambda$ w.r.t. $D$ is the structural obstruction that keeps the coupled cost from collapsing to a flat product. The reduction therefore closes the gap between the scalar certificates (ambient $n=2$) and the full $n$-dimensional projector calculus used throughout the cost stack. No open scaffolding remains on this identity itself; it is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.