elementaryPosting_divF_eq_unitDipole
plain-language theorem explainer
The site-divergence of a single a→b recognition posting equals the unit dipole source (+1 at a, −1 at b). Anyone connecting pair-kernel currents to the finite Dirichlet action cites this identification. The proof unfolds both sides and evaluates two indicator sums by case split on the evaluation site.
Claim. For any lattice size $n$ and sites $a,b,i\in\{0,\ldots,n-1\}$, the site-divergence of the elementary posting current from $a$ to $b$ equals the unit dipole: $\mathrm{div}\,F^{a\to b}(i)=\mathbf{1}_{i=a}-\mathbf{1}_{i=b}$. This holds even when $a=b$.
background
Door 2 of the pair-kernel provenance 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)$. The elementary posting is the double-entry witness of one recognition event: $+1$ on the ordered pair $(a,b)$, $-1$ on $(b,a)$, and $0$ elsewhere.
Independently, the continuum-bridge side of the simplicial ledger defines the unit dipole source as $\mathbf{1}{i=a}-\mathbf{1}{i=b}$. The module's null test already shows that antisymmetry is load-bearing: a constant non-antisymmetric flow has total divergence $n^2\neq 0$. Global and regional discrete Gauss laws then follow from antisymmetry alone.
This theorem equates the two source presentations so that continuity statements written in posting language match those written for the finite Dirichlet action.
proof idea
Unfold divF, elementaryPosting, and unitDipole. The left-hand side becomes $\sum_j\bigl(\mathbf{1}{i=a\land j=b}-\mathbf{1}{i=b\land j=a}\bigr)$. Split the sum by Finset.sum_sub_distrib into a forward indicator sum and a backward indicator sum.
Each sum collapses by a case split on whether the evaluation site equals the source (resp. sink): the forward sum equals $\mathbf{1}{i=a}$ and the backward sum equals $\mathbf{1}{i=b}$. Subtracting yields the unit dipole. No external lemmas beyond definitional unfolding and finite-sum distributivity are required.
why it matters
In the discrete Gauss vertebra, elementary postings are the atomic double-entry currents whose divergences should be the $\pm 1$ sources of recognition bookkeeping. Matching that divergence to the independently defined unit dipole closes the bridge between pair-kernel flux and the source term used by the finite Dirichlet action on the simplicial ledger.
The module doc lists this identification among the axiom-clean results that support continuity: once $\mathrm{div}F=\sigma$ for an antisymmetric $F$, global $\sum\sigma=0$ follows, and the regional form is source-in-region equals boundary flux. Including the degenerate case $a=b$ (both sides zero) keeps the dictionary total.
No downstream consumers are wired yet in the graph; the natural parents are continuity and Dirichlet-action pairing lemmas that treat unit dipoles as test sources. Framework-wise this is ledger infrastructure under Door 2, not a T0–T8 forcing step, but it makes the double-entry structure of recognition events available to continuum-bridge arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.