error_sum_tendsto_zero
plain-language theorem explainer
If each of N error terms is bounded by C/N², their signed sum tends to 0 as N→∞. Phase 4 remainder estimates cite this when curved-spectrum perturbations carry signs rather than absolute values. The argument squeezes the signed sum between the absolute-error sum (already known to vanish) and its negative.
Claim. Let $g:\mathbb{N}\to\mathbb{N}\to\mathbb{R}$ and $C\in\mathbb{R}$. Suppose that for every $N\in\mathbb{N}$ and every $k<N$, $|g(N,k)|\le C/N^{2}$. Then $\sum_{k=0}^{N-1} g(N,k)\to 0$ as $N\to\infty$.
background
This module is the Phase 2a quadrature-limit toolkit for the QG full-theory campaign: elementary uniform-mesh Riemann and lattice sums proved from Heine-Cantor uniform continuity, without relying on Mathlib's tagged-partition BoxIntegral machinery.
The immediate upstream result is the absolute remainder collapse: if $|g(N,k)|\le C/N^{2}$ for all $k<N$, then $\sum_{k<N}|g(N,k)|\to 0$ (total error at most $C/N$). That lemma is load-bearing for Phase 4 curved perturbations of the flat spectrum, which enter as $O(1/N^{2})$ per mode.
The present statement keeps the same per-term bound and upgrades the conclusion from the absolute sum to the signed sum $\sum_{k<N} g(N,k)$. Phase 4 needs the signed form whenever remainder terms are not a priori non-negative.
proof idea
Invoke the absolute collapse lemma to obtain $\sum_{k<N}|g(N,k)|\to 0$. Apply the triangle inequality $|\sum g|\le\sum|g|$ and squeeze $|\sum g|$ to 0 between the zero function and that absolute sum. Negate the limit to get $-|\sum g|\to 0$. Sandwich the signed sum between $-|\sum g|$ and $|\sum g|$ via the standard comparison $-|x|\le x\le|x|$, and conclude by the two-sided squeeze for filters.
why it matters
Closes the signed half of the Phase 2a remainder toolkit. The absolute sibling already forces total error $O(1/N)$; this form is what Phase 4 remainder estimates consume when curved-operator perturbations carry signs. Module documentation lists it as the signed companion of the absolute collapse lemma, generalizing earlier scoped quadrature reductions that only packaged the limit as a hypothesis structure. No downstream Lean consumers are wired yet (used_by is empty), so its campaign value is as the ready signed interface for those Phase 4 estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.