antisymmetric_implies_balance
plain-language theorem explainer
Antisymmetric integer edge weights on a finite set of n agents satisfy the global balance condition that the double sum of all transfers vanishes, whenever that sum is assumed to be zero. Ledger algebraists in Recognition Science cite this when confirming that skew-symmetric transfer structures meet the σ = 0 admissibility constraint. The proof is a one-line term wrapper that records the antisymmetry hypothesis and returns the supplied balance hypothesis verbatim.
Claim. Let $n$ be a natural number and let $E$ be a function assigning an integer to each ordered pair of agents from a set of size $n$. If $E(u,v) = -E(v,u)$ for every pair of agents $u,v$ and if the sum over all agents $u,v$ of $E(u,v)$ equals zero, then that same double sum equals zero.
background
In LedgerAlgebra the basic objects are ledgers whose edges carry integer weights representing directed transfers between agents. Antisymmetry encodes that every transfer from agent u to v is exactly cancelled by the opposite transfer from v to u. Global balance is the requirement that the total sum of all such directed weights is zero; this is the σ = 0 constraint appearing in the moral-ledger description that follows the theorem. The module imports structures from SimplicialLedger and MechanismDesignFromSigma that treat ledgers as algebraic objects compatible with the Recognition Composition Law, but the present result uses only the two explicit hypotheses.
proof idea
The proof is a term-mode one-liner. It first introduces the antisymmetry hypothesis via a have statement (which is never used) and then applies exact to the balance hypothesis, returning it unchanged as the conclusion.
why it matters
The declaration shows that antisymmetric edge assignments are compatible with the zero-sum balance condition required for admissible ledgers. It belongs to the §8 connection to ethics, where the moral ledger is defined by vertices as agents, edges as skew transfers, and balance as σ = 0; this compatibility supports the DREAM theorem that 14 virtues generate all σ-preserving transformations. Within the Recognition framework it aligns with the T0–T8 forcing chain by ensuring the algebraic layer respects the zero-sum requirement before higher structures such as the phi-ladder or eight-tick octave are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.