constFlow_not_antisym
plain-language theorem explainer
The constant all-ones recognition current on a nonempty finite lattice is not antisymmetric. Reviewers of the discrete Gauss null test cite this as the decoy flow that fails double-entry bookkeeping. The argument is a one-line diagonal evaluation: at a fixed site the value 1 cannot equal its own negative.
Claim. For every natural number $n>0$, the constant current $F\equiv 1$ on $\mathrm{Fin}\,n\times\mathrm{Fin}\,n$ is not antisymmetric: it is false that $F(i,j)=-F(j,i)$ for all sites $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 forced to be a gradient. The load-bearing structure is double-entry: a current is antisymmetric when $F(i,j)=-F(j,i)$ for all sites (every debit has a matching credit). Site divergence is then the net outflow at a vertex.
The module builds a null test before the Gauss theorems. If conservation held for every flow, the law would be vacuous. The uniform decoy constFlow sets $F\equiv 1$ on every ordered pair. This definition is the non-double-entry witness used to show that global sum-of-divergences need not vanish.
Antisymmetry is deliberately weaker than the gradient condition $F(i,j)=\varphi_i-\varphi_j$. All conservation statements downstream use only the sign-flip identity.
proof idea
Term-mode proof by contradiction. Assume the constant current is antisymmetric. Instantiate the universal quantifier at the diagonal pair of the zero site in $\mathrm{Fin},n$ (legal because $n>0$). Unfolding the constant definition yields $1=-1$. A numeric normalization closes the contradiction. No external lemmas are required beyond the two local definitions.
why it matters
This is the first half of the reviewer vacuity check for discrete Gauss. The module doc states the trap explicitly: defining flux as a gradient makes divergence-equals-source a tautology. Keeping $F$ abstract and exhibiting a non-antisymmetric decoy shows that conservation has teeth only when double-entry holds.
Together with the sibling that the constant flow breaks global sum-of-divergence neutrality, it certifies that antisymmetry (not gradient structure) is the engine of $\sum\mathrm{div},F=0$ and of the regional flux theorem. In Recognition terms this is the discrete bookkeeping backbone behind sigma-neutrality: net recognition source over the whole lattice vanishes precisely because every posting is matched.
No downstream edges are recorded yet; the declaration stands as the explicit negative witness inside the Door 2 null-test block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.