elementaryPosting_div_sink
plain-language theorem explainer
At the sink of a single double-entry recognition posting from site a to distinct site b, the site divergence equals −1. Anyone building the discrete Gauss law, unit-dipole sources, or continuity identities for recognition currents cites this. The proof unfolds the posting kernel at the sink row, kills the impossible a=b branch by the distinctness hypothesis, and collapses the remaining indicator sum to −1.
Claim. Fix $n\in\mathbb{N}$ and distinct sites $a,b$ in the finite lattice $\mathrm{Fin}\,n$. Let $F$ be the elementary posting current with $F(a,b)=+1$, $F(b,a)=-1$, and $F=0$ on all other ordered pairs. Then the site divergence satisfies $\mathrm{div}\,F(b)=-1$.
background
This module is Door 2 of the pair-kernel provenance lane: discrete Gauss for recognition flux. The current $F:\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$ is kept abstract and antisymmetric, never forced to be a gradient, so conservation is not the tautology $\Delta\varphi=\mathrm{div}(\nabla\varphi)$.
Site divergence is the net outflow $\mathrm{div}F(i)=\sum_j F(i,j)$. The elementary posting is the double-entry witness of one recognition event: $+1$ on the ordered pair $(a,b)$, $-1$ on $(b,a)$, zero elsewhere. Antisymmetry of that kernel is proved separately; global and regional Gauss then follow from double-entry cancellation alone.
The companion source identity (divergence $+1$ at $a$) pairs with this sink identity to identify the posting with the unit dipole used by the finite Dirichlet action.
proof idea
Unfold $\mathrm{div}F(b)$ as $\sum_j F(b,j)$. For each column $j$, simplify the elementary-posting definition at row $b$: the branch $b=a\land j=b$ is impossible by $a\neq b$, so only the subtracted indicator survives, giving $F(b,j)=-1$ when $j=a$ and $0$ otherwise. Congruence of the finite sum replaces the kernel by that indicator, and the sum collapses to the single term $-1$.
why it matters
Together with the source-side companion, this pins the elementary posting as the unit dipole: divergence $+1$ at the origin of the posting and $-1$ at the sink. That identification is what lets the continuity law read site-divergence as sigma-imbalance without defining sigma as a Laplacian of a potential.
In the Door 2 story it supplies the local generator behind global neutrality $\sum_i\mathrm{div}F(i)=0$ and the regional divergence theorem (source in a region equals boundary flux). Those are the non-vacuous conservation statements forced by antisymmetry alone, i.e. by double-entry bookkeeping of recognition events. No downstream consumers are wired yet in the graph; the lemma is infrastructure for the posting layer and any later finite Dirichlet or sigma-neutrality arguments that quote the unit dipole explicitly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.