reciprocal_reciprocal
plain-language theorem explainer
The reciprocal operation on a recognition event, which swaps the two agents and inverts the positive ratio, is an involution: applying it twice recovers the original event. Ledger theorists cite this when closing the double-entry structure forced by J-symmetry. The proof is a one-line simplification that unfolds the event definition and invokes the algebraic identity that the inverse of an inverse is the identity.
Claim. Let $e$ be a recognition event between agents $a,b$ with positive ratio $r>0$. Let $e^{-1}$ be the event obtained by swapping the agents and replacing the ratio by $r^{-1}$. Then $(e^{-1})^{-1}=e$.
background
RecognitionEvent records a directed recognition between two agents together with a positive real ratio. The reciprocal map on events swaps source and target while replacing the ratio by its multiplicative inverse, preserving positivity by the upstream fact that the inverse of a positive real is positive. The module shows that J-symmetry in the underlying algebra forces a double-entry ledger in which every event is paired with its counterpart.
proof idea
The proof is a one-line wrapper that applies simp to the definition of reciprocal together with the algebraic fact that the inverse of an inverse equals the original value.
why it matters
The result is invoked directly in the proofs of reciprocal_eq_iff and reciprocal_inj, and supports add_event_balanced_list (which shows that adjoining an event and its reciprocal preserves the balanced_list property) as well as conservation_from_balance (which derives vanishing net flow in any balanced ledger). It supplies the involution property required for the double-entry structure that the module derives from J-symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.