constFlow
plain-language theorem explainer
The uniform all-ones current on a finite lattice of n sites: every ordered pair carries flow value 1. It is the canonical decoy that fails double-entry bookkeeping. Downstream null tests cite it to prove that global conservation of recognition flux is not automatic and requires antisymmetry of the current.
Claim. For each natural number $n$, the constant flow on the complete directed graph with vertex set $\{0,\ldots,n-1\}$ is the map $F:\{0,\ldots,n-1\}^2\to\mathbb{R}$ defined by $F(i,j)=1$ for every ordered pair $(i,j)$.
background
Door 2 of the pair-kernel provenance lane treats discrete Gauss / continuity: the divergence of a recognition current equals local sigma-imbalance, and the lattice-wide sum of sources vanishes. The current $F:\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$ is kept abstract (never forced to be a gradient), so conservation is not a tautology of the form $\Delta\varphi=\mathrm{div}(\nabla\varphi)$.
Site divergence $\mathrm{div}F$ at $i$ is the sum of outgoing $F(i,\cdot)$. Antisymmetry $F(i,j)=-F(j,i)$ encodes double-entry: each debit is a matching credit. The module builds a null test first: is $\sum_i\mathrm{div}F=0$ true for every flow? If yes, the Gauss law would be vacuous. The all-ones current is the counterexample instrument for that check.
proof idea
Pure definition: the constant function returning $1$ on every ordered pair of sites. No lemmas, no tactics; the body is the term fun _ _ => 1.
why it matters
This decoy is the load-bearing null instrument for the discrete Gauss lane. Three sibling theorems apply it: non-antisymmetry of the all-ones current; exact evaluation $\sum_i\mathrm{div}F=n^2$; and the conservation-break theorem stating that for $n>0$ the global sum of divergences is nonzero. Together they show antisymmetry is necessary for $\sum\mathrm{div}F=0$, so the double-entry hypothesis in the global and regional Gauss laws is not decorative. That clears the vacuity trap flagged in the module: conservation has teeth precisely because non-antisymmetric flows fail it. Downstream, the genuine theorems (antisym sum-to-zero, global Gauss, regional divergence theorem, sigma neutrality from continuity) rest on that contrast.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.