reciprocal_reciprocal
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute or bound the J-cost of any event.
- Does not apply to structures lacking a positive ratio field.
- Does not establish injectivity or uniqueness of the reciprocal map.
- Does not address higher-order ledger properties such as conservation laws.
Lean usage
rw [reciprocal_reciprocal]formal statement (Lean)
56theorem reciprocal_reciprocal (e : RecognitionEvent) : reciprocal (reciprocal e) = e := by
proof body
One-line wrapper that applies simp.
57 simp only [reciprocal, inv_inv]
58