divF
plain-language theorem explainer
Site divergence of a recognition current on a finite lattice: at each site i, sum the outgoing pair fluxes F(i,j) over all targets j. Anyone citing the discrete Gauss law, global sigma neutrality, or elementary double-entry postings uses this as the local source term. The body is a one-line Finset sum, not a derived identity.
Claim. For a finite lattice of $n$ sites and a real-valued pair current $F:\{0,\ldots,n-1\}^2\to\mathbb{R}$, the site divergence at $i$ is $(\mathrm{div}\,F)(i):=\sum_j F(i,j)$, the net recognition outflow from $i$.
background
This module is Door 2 of the pair-kernel provenance lane: after shift-invariant pair cost and the locality hypothesis, the next step is a discrete Gauss/continuity law. The recognition current $F$ is kept abstract (any map $F:\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$), never forced to be a gradient $\nabla\varphi$. That avoids the vacuity trap where $\mathrm{div}(\nabla\varphi)=\Delta\varphi$ is an identity with no conservation content.
Site divergence is the local bookkeeping object: net outflow from account $i$. Antisymmetry $F(i,j)=-F(j,i)$ encodes double-entry (each debit is a matching credit). Global conservation $\sum_i(\mathrm{div},F)(i)=0$ and the regional form (source in a region equals boundary flux) are proved from antisymmetry alone. A uniform non-antisymmetric decoy current is used first as a null test to show the Gauss law has teeth.
proof idea
Pure definition: unfold to the finite sum $\sum_{j:\mathrm{Fin},n} F,i,j$. No lemmas, no tactics. Downstream proofs typically simp or unfold divF and then apply Finset sum identities or the antisymmetry cancellation lemmas in this module.
why it matters
This is the local source term that makes the discrete Gauss law speak recognition language rather than graph-Laplacian tautology. Downstream it feeds the null test (constFlow_sum_div, constFlow_breaks_conservation), global Gauss (sum_divF_zero), regional divergence theorem (sum_divF_region_eq_boundary_flux), continuity-implies-sigma-neutrality (sigma_sum_zero_of_continuity), and the elementary a→b posting calculus (elementaryPosting_div_source/sink, elementaryPosting_divF_eq_unitDipole, elementaryPosting_sum_div_zero).
In framework terms it is the discrete avatar of continuity: site-divergence equals sigma-imbalance, and integrating forces global sigma = 0 neutrality from double-entry alone. That is the conservation content of recognition events before continuum or Clifford structure is layered on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.