sum_divF_zero
plain-language theorem explainer
On any finite lattice, the sum of site divergences of an antisymmetric recognition current vanishes. This is the global discrete Gauss law: net recognition source is zero by double-entry bookkeeping alone, with no potential assumed. Anyone citing sigma-neutrality or continuity-implies-global-conservation needs it. The proof unfolds the divergence definition and applies double-entry cancellation on the full vertex set.
Claim. Let $F:\{0,\ldots,n-1\}^2\to\mathbb{R}$ satisfy $F(i,j)=-F(j,i)$ for all $i,j$. Writing $\mathrm{div}\,F(i)=\sum_j F(i,j)$ for the net outflow at site $i$, one has $\sum_i \mathrm{div}\,F(i)=0$.
background
Door 2 of the pair-kernel lane treats recognition flux as an abstract current $F$ on a finite vertex set, not as a gradient of a potential. The module keeps $F$ free and imposes only antisymmetry: every debit at one account is a matching credit at another. Site divergence $\mathrm{div} F(i)$ is the net outflow $\sum_j F(i,j)$.
The vacuity trap is explicit: if one defined $F=\nabla\varphi$ and source as the graph Laplacian, "divergence equals source" would be tautological. Here conservation is the real content, and it is load-bearing. The null test constFlow_breaks_conservation shows a constant non-antisymmetric flow has total divergence $n^2\neq 0$.
The engine lemma is double-entry cancellation on any region $S$: $\sum_{i\in S}\sum_{j\in S} F(i,j)=0$ for antisymmetric $F$. Global Gauss is that identity on the full lattice, rewritten in divergence language.
proof idea
Term-mode, two steps. Unfold $\mathrm{div} F(i)=\sum_j F(i,j)$, so the left-hand side is the double sum of $F$ over the full vertex set. Invoke antisym_sum_finset_zero on $S=\mathrm{univ}$: any antisymmetric current sums to zero over every region, hence over the whole lattice. A simpa closes the identification.
why it matters
This is the global discrete Gauss law in the pair-kernel provenance lane: net recognition source over the lattice is zero, forced by double-entry antisymmetry rather than by any potential $\varphi$. It is the sigma $=0$ conservation law stated on the current side.
Downstream, sigma_sum_zero_of_continuity lifts the same neutrality to any source that equals site divergence of an antisymmetric current, without ever setting $\sigma:=\Delta\varphi$. The elementary a→b posting uses it via elementaryPosting_sum_div_zero to show a single double-entry event conserves globally.
Together with the regional form (source in a region equals boundary flux), it supplies the discrete continuity skeleton that later couples to the recognition composition law and the forcing chain, while remaining axiom-clean and free of gradient tautologies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.