elementaryPosting
plain-language theorem explainer
The elementary a→b recognition current puts +1 on the ordered pair (a,b), −1 on (b,a), and 0 elsewhere. It is the atomic double-entry witness for one recognition posting, built from postings rather than from a potential. Anyone proving discrete Gauss, sigma-neutrality, or dipole sources on the finite ledger cites it. The body is a two-branch indicator difference; no proof is required.
Claim. For $n \in \mathbb{N}$ and accounts $a,b \in \{0,\ldots,n-1\}$, the elementary posting current $F_{a\to b}:\{0,\ldots,n-1\}^2\to\mathbb{R}$ is $F_{a\to b}(i,j)=\mathbf{1}_{i=a,j=b}-\mathbf{1}_{i=b,j=a}$.
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 $\nabla\varphi$. The module's point is that conservation is load-bearing: antisymmetry $F(i,j)=-F(j,i)$ is exactly double-entry bookkeeping (each debit at one account is a matching credit at another). The null test is that a constant non-antisymmetric flow has nonzero total divergence, so global $\sum\mathrm{div},F=0$ is not vacuous.
Site divergence $\mathrm{div}F(i)=\sum_j F(i,j)$ is the local source. The elementary posting is the atomic current realizing one recognition event from account $a$ to $b$. Downstream lemmas read its divergence as a unit dipole ($+1$ at the source, $-1$ at the sink when $a\neq b$) and recover global neutrality from antisymmetry alone.
proof idea
Pure definition: the map $(i,j)\mapsto \mathbf{1}{i=a\land j=b}-\mathbf{1}{i=b\land j=a}$. No tactics, no lemmas. Unfolding is the only step later proofs need.
why it matters
This is the concrete double-entry witness named in the module doc: a single a→b posting whose divergence is the sigma-imbalance of one recognition event, read off postings rather than $\nabla\varphi$. It feeds elementaryPosting_antisym (antisymmetry), elementaryPosting_sum_div_zero (global conservation via sum_divF_zero), elementaryPosting_div_source / _div_sink ($+1$ at $a$, $-1$ at $b$), and elementaryPosting_divF_eq_unitDipole (match to the continuum-bridge unit dipole, including $a=b$).
Outside the foundation lane, Gravity.Analysis.MetricEdgeImage4D uses it as a counterexample: the elementary posting on $\mathrm{Fin},16$ is not in the metric-edge image, separating recognition currents from pure strain currents. In the broader RS chain this is the atomic object behind discrete Gauss and sigma=0 neutrality after the pair-cost carrier and locality hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.