elementaryPosting_antisym
plain-language theorem explainer
The elementary a→b recognition posting is an antisymmetric current on any finite lattice. Anyone building double-entry conservation or discrete Gauss from postings cites this. The proof unfolds the piecewise definition, swaps the conjunctions in the indicator conditions, and finishes by ring.
Claim. For any $n\in\mathbb{N}$ and sites $a,b\in\{0,\ldots,n-1\}$, the elementary posting current $F_{a\to b}$ defined by $F_{a\to b}(i,j)=1$ on the ordered pair $(a,b)$, $-1$ on $(b,a)$, and $0$ elsewhere, is antisymmetric: $F_{a\to b}(i,j)=-F_{a\to b}(j,i)$ for all sites $i,j$.
background
This module is Door 2 of the pair-kernel provenance lane: discrete Gauss for recognition flux. After the pair-cost carrier and locality, the content is that divergence of a recognition current equals local sigma-imbalance, with global integral zero. The flux $F:\mathrm{Fin},n\to\mathrm{Fin},n\to\mathbb{R}$ is kept abstract and never forced to be a gradient, so conservation is not the tautology $\Delta\varphi=\mathrm{div}(\nabla\varphi)$.
Antisymmetry is the double-entry structure: flow from $i$ to $j$ equals minus flow from $j$ to $i$. The null test is that a constant non-antisymmetric flow breaks global conservation ($\sum\mathrm{div}F=n^2\neq 0$). The elementary posting is the atomic witness: $+1$ on $(a,b)$, $-1$ on $(b,a)$, zero elsewhere, built from postings rather than a potential.
proof idea
Tactic proof, not a wrapper. Introduce arbitrary sites $i,j$, unfold the elementary posting into the difference of two indicators, then apply and_comm twice so the swapped-index conditions match the antisymmetry goal. simp only rewrites those biconditionals; ring closes the resulting real arithmetic identity $x-y=-(y-x)$ on the indicator values.
why it matters
This is the double-entry witness for a single recognition event in the discrete Gauss stack. Downstream, elementaryPosting_sum_div_zero applies global Gauss (sum_divF_zero) to this antisymmetry fact, so one posting has vanishing total divergence. That feeds the concrete debit/credit source law ($+1$ at $a$, $-1$ at $b$).
In gravity analysis, elementaryPosting_not_in_MetricEdgeImage uses the same posting to separate pure double-entry currents from the image of metric-edge strain currents on a 4D edge set. Within the framework, antisymmetry is load-bearing for sigma-neutrality and the regional divergence theorem; without it the conservation law has no teeth. The result is axiom-clean scaffolding for continuity without defining sources as Laplacians.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.