elementaryPosting_sum_div_zero
plain-language theorem explainer
A single elementary recognition posting from site a to site b has vanishing total site-divergence on any finite lattice. Cite this when treating atomic double-entry events as conserved recognition currents. The argument is a one-line specialization of the global discrete Gauss law to the antisymmetry of that elementary current.
Claim. For every $n\in\mathbb{N}$ and sites $a,b\in\mathrm{Fin}\,n$, if $F^{a\to b}$ is the elementary posting current ($+1$ on the ordered pair $(a,b)$, $-1$ on $(b,a)$, and $0$ elsewhere), then $\sum_{i}\mathrm{div}\,F^{a\to b}(i)=0$.
background
Door 2 of the pair-kernel lane treats recognition flux as an abstract antisymmetric 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 forced by antisymmetry alone (double-entry: every debit is a matching credit).
The elementary posting is the atomic witness: $+1$ on $(a,b)$, $-1$ on $(b,a)$, zero elsewhere. It is built from postings, not from $\nabla\varphi$, so the Gauss identity is not the tautology $\Delta\varphi=\mathrm{div}(\nabla\varphi)$. A null test already shows the uniform non-antisymmetric flow $F\equiv 1$ has total divergence $n^2\neq 0$, so antisymmetry is load-bearing.
Upstream, sum_divF_zero states the global discrete Gauss law for any antisymmetric current; elementaryPosting_antisym records that the elementary posting is antisymmetric.
proof idea
One-line term wrapper. Feed the antisymmetry certificate for the elementary $a\to b$ posting into the global Gauss theorem: any antisymmetric current has vanishing total site-divergence. No extra algebra on the posting itself is required.
why it matters
Closes the conservation half of the elementary-posting package in the discrete Gauss module: a single $a\to b$ recognition event is an antisymmetric current whose integrated source is zero. Together with the companion source readout (divergence $+1$ at $a$ and $-1$ at $b$ when $a\neq b$), this is the double-entry witness read off postings rather than off $\nabla\varphi$.
That package supports the module's continuity story: site-divergence equals sigma-imbalance, and integrating yields the sigma $=0$ neutrality law without ever defining sigma as a Laplacian. The regional form (source in a region equals boundary flux) sits one step above the same antisymmetry engine. No downstream dependents are wired yet; the result is a local vertebra in the pair-kernel provenance lane after shift-invariant pair cost and finite-range locality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.