sum_twoSparse
plain-language theorem explainer
A weighted sum of squared coordinates of a 2-sparse vector collapses exactly to the two support terms. Anyone lifting closed-form 2D scalar identities for the projector P_λ (or its μ-scalar and sharp-dot) to ambient dimension n cites this lemma. The proof zeros every off-support summand from the TwoSparse hypothesis, then reduces the Finset sum to a two-element pair.
Claim. Let $\alpha\in\mathbb{R}^n$ vanish outside two distinct indices $i_0\neq i_1$, and let $f$ be any real function on the coordinate set. Then $\sum_i f(i)\,\alpha_i^2 = f(i_0)\,\alpha_{i_0}^2 + f(i_1)\,\alpha_{i_1}^2$.
background
The module lifts 2D scalar certificates for the projector $P_\lambda$ to arbitrary ambient dimension $n$. In the 2D setup one works with $\alpha=(a,b)$; the general-$n$ analogue is the predicate TwoSparse: $\alpha_k=0$ whenever $k\notin{i_0,i_1}$. Vectors are coordinate maps $\mathrm{Vec},n=\mathrm{Fin},n\to\mathbb{R}$.
The inverse-metric kernel used throughout is $D^{-1}t$, the diagonal inverse of the undeformed Hessian $D=\mathrm{diag}(\cosh t_0,\ldots,\cosh t_{n-1})$. Projector and curvature scalars are built from weighted sums of the form $\sum_i f(i),\alpha_i^2$. Once $\alpha$ is 2-sparse those sums must collapse algebraically to two terms, so that every closed-form identity proved on the 2D slice remains valid as an identity of functions at general $n$, not merely up to isomorphism.
proof idea
Tactic proof on Finsets. First record that ${i_0,i_1}\subseteq\mathrm{univ}$. Then show every summand with index outside that pair vanishes: the TwoSparse hypothesis forces $\alpha_x=0$, so $f(x)\alpha_x^2=0$ by ring. Rewrite the full sum via Finset.sum_subset using that vanishing lemma, and finish with Finset.sum_pair on the distinct indices $i_0\neq i_1$. No analysis or metric structure is used; the argument is pure finite-sum algebra.
why it matters
This is the general-$n$ mechanism named in the module doc: every closed-form 2D scalar identity becomes valid at arbitrary ambient dimension once support is restricted to two coordinates. Immediate parents are mu_Dinv_twoSparse (the $\mu_\lambda$ scalar of Projector collapses to the two-term form with $D^{-1}t$) and dot_sharp_Dinv_twoSparse in CurvatureBridge (the quadratic form $S=\alpha\cdot D^{-1}\alpha$ likewise collapses). Both feed the block-diagonal reduction of $P_\lambda$ and the mixed Riemann path (RiemannMixedApply).
Together they underwrite the algebraic identity PApply_e_eq_P00Gen and the transport of non-parallelism (Theorem 1a / PApply_not_parallel_gen) from the 2D slice to general $n$. In the Recognition cost stack this is the Christoffel/projector-component block reduction that lets 2D certificates control the full $n$-dimensional operator algebra without re-proving each identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.