reciprocal_eq_iff
plain-language theorem explainer
reciprocal_eq_iff establishes that for any two recognition events the reciprocal of the first equals the second exactly when the first equals the reciprocal of the second. Ledger-forcing arguments in Recognition Science cite it to guarantee that the swap-and-invert map is an involution, which is required for double-entry balance. The proof splits the biconditional with constructor and rewrites each direction by the already-proved fact that reciprocal twice recovers the original event.
Claim. Let $x$ and $e$ be recognition events (pairs of agents with a positive real ratio). Then the event obtained by swapping agents and inverting the ratio of $x$ equals $e$ if and only if $x$ equals the swapped-and-inverted version of $e$.
background
RecognitionEvent is the structure recording a directed recognition between two agents: source and target natural numbers together with a positive real ratio. The reciprocal operation on such an event swaps source and target while replacing the ratio by its multiplicative inverse, preserving positivity. The module LedgerForcing shows that J-symmetry of the cost function forces this reciprocal to behave like a double-entry ledger. The key supporting fact is the theorem reciprocal_reciprocal, which states that applying the swap-and-invert map twice returns the original event.
proof idea
The proof is a direct constructor that splits the biconditional into two implications. Each implication substitutes the hypothesis and rewrites with the already-established reciprocal_reciprocal lemma, which cancels the double application of the involution.
why it matters
The result supplies the involution property needed to close the symmetry argument that turns J-symmetry into balanced double-entry ledgers. It sits inside the chain that derives ledger structure from the Recognition Composition Law and the definition of J. Because the used-by list is empty, the lemma remains available for later ledger-balance theorems rather than being consumed inside this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.