reciprocal_inj
The reciprocal map on recognition events is injective. Ledger theorists in Recognition Science cite this to ensure events are uniquely recoverable from their reciprocals when enforcing balance. The proof is a direct algebraic reduction that applies the involution property twice.
claimLet $x$ and $e$ be recognition events. Then the reciprocal event of $x$ equals the reciprocal event of $e$ if and only if $x = e$.
background
The Ledger Forcing module establishes that J-symmetry induces double-entry ledger structure. A RecognitionEvent is a structure recording source agent, target agent, and positive real ratio. The reciprocal map swaps source and target while inverting the ratio, modeling symmetric recognition from the opposite agent. This rests on the reciprocal automorphism defined in CostAlgebra and on the upstream theorem that reciprocal of reciprocal recovers the original event.
proof idea
The term-mode proof splits the biconditional with constructor. The forward direction rewrites the hypothesis using the reciprocal_reciprocal lemma on both sides to recover the original equality. The reverse direction substitutes directly.
why it matters in Recognition Science
This injectivity supports the downstream balance theorems add_event_balanced_list and conservation_from_balance, which pair each event with its reciprocal to obtain zero net flow. It closes a step in the J-symmetry forcing chain by guaranteeing that ledger operations remain invertible, consistent with the Recognition Composition Law and the double-entry structure derived from it.
scope and limits
- Does not prove surjectivity of the reciprocal map.
- Does not address continuous or non-discrete recognition models.
- Does not establish computational matching algorithms for events.
- Does not extend injectivity to composite ledger operations.
Lean usage
have h : reciprocal x = reciprocal e := by sorry; exact (reciprocal_inj x e).mp hformal statement (Lean)
64theorem reciprocal_inj (x e : RecognitionEvent) : reciprocal x = reciprocal e ↔ x = e := by
proof body
Term-mode proof.
65 constructor
66 · intro h; rw [← reciprocal_reciprocal x, h, reciprocal_reciprocal]
67 · intro h; rw [h]
68
69/-- The cost of a recognition event. -/