constFlow_sum_div
plain-language theorem explainer
On a lattice of n sites, the uniform all-ones current has total site-divergence equal to n squared. Anyone checking that the discrete Gauss law is not vacuous cites this identity: it evaluates the decoy flow that fails double-entry. The proof is a short simplification unfolding divergence and the constant current, then counting the Fin n universe.
Claim. For every natural number $n$, if $F$ is the constant current $F(i,j)=1$ on $\mathrm{Fin}\,n\times\mathrm{Fin}\,n$, then $\sum_{i}\mathrm{div}\,F(i)=n\cdot n$ in $\mathbb{R}$, where site divergence is $\mathrm{div}\,F(i)=\sum_j F(i,j)$.
background
Door 2 of the pair-kernel lane treats recognition flux as an abstract current $F:\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$, never as a gradient of a potential. Site divergence is the net outflow $\mathrm{div}F(i)=\sum_j F(i,j)$. Global conservation $\sum_i\mathrm{div}F(i)=0$ is the discrete Gauss / sigma-neutrality law, and it is forced by antisymmetry $F(i,j)=-F(j,i)$ (double-entry), not by any Laplacian identity.
The module builds a null test first: is $\sum\mathrm{div}F=0$ true for every flow? The uniform current $\mathrm{constFlow},n$, defined by $F\equiv 1$, is the decoy. It is not antisymmetric. This lemma computes its total divergence exactly, so the next theorem can show the sum is nonzero whenever $n>0$.
proof idea
Term-mode simplification. Unfold site divergence and the constant current, so each summand is $\sum_j 1$. Rewrite the outer sum as a constant sum over the universe of $\mathrm{Fin},n$, replace cardinality by $n$, convert $n\bullet 1$ to multiplication, and finish with $n\cdot 1=n$. No external lemmas beyond the standard Finset/Fintype card and scalar identities are required.
why it matters
Feeds constFlow_breaks_conservation, whose doc-comment states the null test: a non-antisymmetric current breaks global conservation ($\sum\mathrm{div}F\neq 0$), so double-entry is load-bearing in the Gauss law. Without this exact evaluation, the inequality step has nothing to rewrite against.
In the Recognition framework this anchors the discrete continuity law that later yields $\sum\sigma=0$ and the regional divergence theorem (source in a region equals boundary flux). It is the instrument check that conservation is not a tautology of the form $\Delta\phi=\mathrm{div}(\nabla\phi)$, but a genuine consequence of antisymmetric posting structure on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.