sigma_sum_zero_of_continuity
plain-language theorem explainer
If a source field equals the site-divergence of an antisymmetric recognition current, its total sum vanishes. This is global sigma-neutrality stated on the source alone, without defining sigma as a Laplacian. Anyone citing the discrete Gauss / continuity lane (Door 2) uses it to lift conservation from currents to abstract imbalances. The proof rewrites the sum by continuity and applies global discrete Gauss.
Claim. Let $F:\{0,\ldots,n-1\}^2\to\mathbb{R}$ be antisymmetric ($F_{ij}=-F_{ji}$ for all $i,j$) and let $\sigma$ satisfy $\mathrm{div}\,F(i)=\sigma_i$ at every site $i$, where $\mathrm{div}\,F(i)=\sum_j F_{ij}$. Then $\sum_i\sigma_i=0$.
background
This module is the Door 2 discrete Gauss vertebra of the pair-kernel provenance lane. After shift-invariant pair cost and the locality hypothesis, the next law is continuity: site-divergence of the recognition current equals local sigma-imbalance, and the global integral of that source is zero.
The current $F$ is kept abstract: a free map $\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$, never forced to be a gradient $\nabla\varphi$. Antisymmetry ($F_{ij}=-F_{ji}$) is the double-entry structure of a recognition event (every debit has a matching credit). Site divergence is $\mathrm{div},F(i)=\sum_j F_{ij}$. A null test shows the law has teeth: the constant flow $F\equiv 1$ is not antisymmetric and has $\sum\mathrm{div},F=n^2\neq 0$.
Upstream, sum_divF_zero already proves $\sum_i\mathrm{div},F(i)=0$ for any antisymmetric $F$, via pairwise cancellation over the full lattice. The present result only renames that total divergence as an external source $\sigma$.
proof idea
Two steps. First, Finset sum congruence: continuity $\mathrm{div},F(i)=\sigma_i$ at each $i$ rewrites $\sum_i\sigma_i$ as $\sum_i\mathrm{div},F(i)$ (symmetry of equality). Second, apply the global discrete Gauss theorem: any antisymmetric current has vanishing total divergence. No expansion of $\mathrm{div},F$ and no region/boundary split are needed.
why it matters
Closes the continuity-to-neutrality arrow in the discrete Gauss package without the vacuity trap of defining $\sigma:=\Delta\varphi$. The module doc lists it among the axiom-clean results: site-divergence equals sigma-imbalance implies global sigma neutrality, forced only by double-entry antisymmetry.
That neutrality is the sigma $=0$ conservation law on the source side of the ledger. It sits beside the regional divergence theorem (source in a region equals boundary flux) and the elementary posting witness (a single $a\to b$ posting is an antisymmetric current with $\mathrm{div}=+1$ at $a$ and $-1$ at $b$). No downstream consumers are wired yet in the graph; the declaration is a leaf that packages the conservation content for later continuity or ledger arguments.
In the broader Recognition chain this is foundation plumbing for double-entry recognition events, not a T5–T8 forcing step, but it is the discrete reason net source cannot appear from pure pair postings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.