sum2_restrict_pair
plain-language theorem explainer
A double sum over Fin n × Fin n of a real bivariate array collapses to its four values on a distinguished 2×2 block whenever the array vanishes off that block in either argument. Curvature reductions cite it to kill spectator indices in Shima-type Riemann sums. The proof applies the single-index restriction lemma once per row, then once per remaining column.
Claim. Fix $n\in\mathbb{N}$ and distinct indices $i_0,i_1\in\{0,\ldots,n-1\}$. Let $f:(\mathrm{Fin}\,n)^2\to\mathbb{R}$ satisfy $f(p,q)=0$ whenever $p\notin\{i_0,i_1\}$ or $q\notin\{i_0,i_1\}$. Then $\sum_p\sum_q f(p,q)=f(i_0,i_0)+f(i_1,i_0)+f(i_0,i_1)+f(i_1,i_1)$.
background
This module lifts Theorem 2 (non-flatness of the deformed Hessian metric $h_\lambda$) from the 2D scalar certificates to arbitrary ambient dimension $n$. Metrics, inverses, third derivatives $\beta$, and mixed Riemann components are bare arrays on $\mathrm{Fin},n$, with curvature given by Shima's formula
$R_{ijkl}=(1/4)\sum_{p,q}h^{pq}(\beta_{jkp}\beta_{ilq}-\beta_{ikp}\beta_{jlq})$,
and $R^i{}{jkl}=\sum_m h^{im}R{mjkl}$.
The single-index companion lemma states that if $g:\mathrm{Fin},n\to\mathbb{R}$ vanishes off ${i_0,i_1}$, then $\sum_k g(k)=g(i_0)+g(i_1)$. The present result is the bivariate analogue needed when both free indices of a summand in Shima's double sum are constrained by two-sparsity of $\alpha$ (support on at most two coordinates) and by the diagonal structure of the undeformed inverse $D^{-1}=\mathrm{diag}((\cosh t_i)^{-1})$.
proof idea
For each fixed row index $p$, the inner sum $\sum_q f(p,q)$ is a single-index sum whose summand vanishes off ${i_0,i_1}$ by the right half of the bivariate vanishing hypothesis. Apply the single-index restriction lemma to obtain $\sum_q f(p,q)=f(p,i_0)+f(p,i_1)$.
Rewrite the double sum via congruence and additivity as $\sum_p f(p,i_0)+\sum_p f(p,i_1)$. Each of those outer sums again vanishes off ${i_0,i_1}$ (left half of the hypothesis), so two more applications of the single-index lemma yield the four-term right-hand side.
why it matters
Feeds the Stage B capstone RiemannMixedApply_reduce: under two-sparse $\alpha$ supported on ${i_0,i_1}$ and $t_{i_1}=0$, the general-$n$ mixed component $R^{i_0}{}_{i_1,i_0,i_1}$ built from the actual deformed metric and inverse via Shima collapses algebraically to the closed form $R0101Gen$ already certified negative in the 2D scalar certificates. That is the general-$n$ non-flatness content of Theorem 2.
Without this double-sum collapse, spectator indices in the $h^{pq}\beta\beta$ sums would survive and the reduction to the certified 2D formula would not go through by pure array arithmetic. The module architecture deliberately avoids abstract totally-geodesic restriction arguments; this lemma is the elementary sum-manipulation step that keeps the proof panel-greenlit and bare-array throughout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.