constFlow_breaks_conservation
plain-language theorem explainer
On a finite lattice of size n>0, the uniform all-ones current has nonzero total site-divergence (equal to n²). Anyone citing the discrete Gauss / double-entry lane uses this as the null test that conservation is not automatic. The proof rewrites the sum via the closed-form identity for that current and notes that n·n is strictly positive.
Claim. For every natural number $n>0$, if $F$ is the constant current $F_{ij}\equiv 1$ on the complete digraph with $n$ sites, then $\sum_{i=1}^{n}\mathrm{div}\,F(i)\neq 0$.
background
This module develops the discrete Gauss / continuity law for recognition flux: site-divergence equals local sigma-imbalance, and the global integral of sources vanishes. The flux $F:\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$ is kept abstract (never forced to be a gradient), so conservation is genuine content rather than the tautology $\Delta\varphi=\mathrm{div}(\nabla\varphi)$.
Site divergence is the net outflow $\mathrm{div}F(i)=\sum_j F(i,j)$. The constant current $\mathrm{constFlow}$ is the decoy $F\equiv 1$, which is not antisymmetric. Its total divergence is computed upstream as $\sum_i\mathrm{div}F(i)=n\cdot n$. The module's stated purpose for this lemma is the vacuity check: global conservation $\sum\mathrm{div}F=0$ must fail for some non-antisymmetric flow, or else the later Gauss theorems would be null tests.
proof idea
One short tactic proof. Rewrite the sum by the closed identity constFlow_sum_div, which evaluates $\sum_i\mathrm{div}(\mathrm{constFlow},n)(i)$ to $n\cdot n$. Cast the hypothesis $0<n$ to a positivity fact on $\mathbb{R}$, then apply positivity of a product of two positive reals to conclude $n\cdot n\neq 0$.
why it matters
This is the null test built first in the Door-2 discrete Gauss lane. The module doc states the trap explicitly: if conservation held for every current, the double-entry (antisymmetry) hypothesis would be vacuous. Showing that $F\equiv 1$ yields $\sum\mathrm{div}F=n^2\neq 0$ proves antisymmetry is load-bearing for the global Gauss law sum_divF_zero, the regional divergence theorem sum_divF_region_eq_boundary_flux, and the continuity consequence sigma_sum_zero_of_continuity.
In Recognition Science terms this anchors the bookkeeping side of recognition events: each debit at one account is a matching credit at another. Without that cancellation, net source need not vanish. No downstream dependents are recorded yet; the lemma's role is justificatory for the conservation theorems that follow in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.