sum_restrict_pair
plain-language theorem explainer
A real-valued function on Fin n that vanishes off a two-point support {i0,i1} has total sum equal to the sum of its two support values. Curvature and block-reduction arguments cite it whenever a sparse sum must collapse before applying Shima's formula. The proof is a short Finset argument: subset the two-point set, zero off it, then sum_pair.
Claim. Let $n\in\mathbb{N}$ and let $i_0,i_1\in\{0,\ldots,n-1\}$ with $i_0\neq i_1$. If $f:\{0,\ldots,n-1\}\to\mathbb{R}$ satisfies $f(k)=0$ whenever $k\neq i_0$ and $k\neq i_1$, then $\sum_{k} f(k)=f(i_0)+f(i_1)$.
background
The module lifts Theorem 2 (non-flatness of the deformed Hessian metric $h_\lambda$) from a 2-D slice to arbitrary ambient dimension $n$. It builds the bare-array deformed metric $h_\lambda=D+\lambda\tilde g$, its Sherman-Morrison inverse, the third-derivative tensor $\beta_{ijk}=\partial_i\partial_j\partial_k\Phi$, and the mixed Riemann components via Shima's formula
$R_{ijkl}=\frac14\sum_{p,q}h^{pq}(\beta_{jkp}\beta_{ilq}-\beta_{ikp}\beta_{jlq})$,
then $R^i{}{jkl}=\sum_m h^{im}R{mjkl}$. All objects are plain functions on Fin n, not manifold API.
Under a two-sparse deformation parameter $\alpha$ supported on ${i_0,i_1}$, many intermediate sums in that construction are zero off that pair. This lemma is the unweighted single-index form of that collapse (the weighted sibling lives in BlockReduction as the two-sparse sum identity). It is stated for a bare $f$ so the same fact can be reused inside the Riemann reduction without carrying $\alpha_i^2$ weights.
proof idea
Form the two-element Finset ${i_0,i_1}$, which is a subset of the universe. Rephrase the vanishing hypothesis as: every universe element outside that pair has $f=0$. Rewrite the full sum as the sum over the pair via Finset.sum_subset, then apply Finset.sum_pair (using $i_0\neq i_1$) to obtain $f(i_0)+f(i_1)$. No analysis or metric structure is used; it is pure finite-sum bookkeeping.
why it matters
The lemma is the single-sum engine under the Stage B curvature bridge. Its double-sum sibling sum2_restrict_pair applies it once per outer index, collapsing $\sum_p\sum_q f(p,q)$ to the four values on ${i_0,i_1}^2$. That double restriction is what lets the general-$n$ mixed component $R^{i_0}{}_{i_1,i_0,i_1}$, built from the actual $h$ inverse and $\beta$ via Shima, reduce algebraically to the closed scalar form R0101Gen already certified negative in ScalarCertificates.
Downstream, RiemannMixedApply_reduce is the capstone: under TwoSparse $\alpha$ and $t_{i_1}=0$, the abstract $n$-dimensional curvature construction specializes exactly to the certified 2-D non-flatness formula. Without this sparse-sum collapse, the $n$-sum in Shima's formula would not peel down to the two-support closed form. The result is infrastructure for the general-$n$ non-flatness claim in the Hessian-cost geometry, not a physics law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.