elementaryPosting_div_source
plain-language theorem explainer
The divergence of a single a-to-b recognition posting equals +1 at the source site a whenever a ≠ b. Anyone citing the discrete Gauss double-entry witness for recognition flux uses this local source reading. The proof unfolds the posting at the source row, collapses it to the indicator of the sink column, and sums.
Claim. For $n\in\mathbb{N}$ and distinct sites $a,b\in\{0,\ldots,n-1\}$, let $F$ be the elementary posting current with value $+1$ on the ordered pair $(a,b)$, $-1$ on $(b,a)$, and $0$ elsewhere. Then the site divergence of $F$ at the source equals one: $\sum_j F(a,j)=1$.
background
This module is the Door 2 / discrete Gauss vertebra of the pair-kernel provenance lane. Currents $F:\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$ stay abstract and antisymmetric; they are never defined as gradients of a potential. That choice avoids the vacuity trap in which $\mathrm{div}(\nabla\varphi)=\Delta\varphi$ is an identity with no conservation content.
Site divergence is net recognition outflow from a site: $\mathrm{div},F(i)=\sum_j F(i,j)$. The elementary posting from $a$ to $b$ is the atomic double-entry current: $+1$ on $(a,b)$, $-1$ on $(b,a)$, zero elsewhere, built from postings rather than from a potential.
Upstream, antisymmetry already forces global $\sum_i\mathrm{div},F(i)=0$ and the regional divergence theorem (source in a region equals boundary flux). The present result pins the local debit at the source of one elementary posting.
proof idea
Site divergence is definitionally the sum of the current over the second index. For fixed source $a\neq b$, a short case analysis shows that the elementary posting at $(a,j)$ equals the indicator $1_{j=b}$: the reverse-pair term requires first index $b$, which is false on this row, so only the forward debit survives. Finite-sum congruence replaces every summand by that indicator; the resulting sum is $1$.
why it matters
With the sibling facts that the elementary posting is antisymmetric and carries divergence $-1$ at the sink, this supplies the double-entry witness named in the module doc: a single $a\to b$ posting has sigma-imbalance $+1$ at $a$ and $-1$ at $b$, read off the postings, not off $\nabla\varphi$. That witness is the concrete carrier for the continuity path (site-divergence equals sigma-imbalance implies global sigma neutrality) inside the discrete Gauss law. No recorded downstream dependents yet; the lemma is a local building block for conservation, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.