reciprocal_inj
plain-language theorem explainer
The reciprocal map on recognition events is injective. Ledger balance proofs cite this result when closing under addition of reciprocal pairs. The proof is a direct algebraic reduction that invokes the involution property to equate the forward direction and substitutes for the converse.
Claim. Let $x$ and $e$ be recognition events. The reciprocal of $x$ equals the reciprocal of $e$ if and only if $x$ equals $e$.
background
The LedgerForcing module establishes that J-symmetry forces double-entry ledger structure. A RecognitionEvent records a directed recognition between two agents via source, target, and positive real ratio. The reciprocal operation swaps the agents and replaces the ratio by its multiplicative inverse, yielding another valid event. This construction rests on the upstream reciprocal_reciprocal theorem, which states that applying the reciprocal twice recovers the original event exactly.
proof idea
The term-mode proof opens with the constructor tactic to split the biconditional. The forward direction rewrites the left-hand side via the reciprocal_reciprocal lemma applied to $x$, substitutes the assumption, then applies the same lemma to the right-hand side. The reverse direction performs a direct substitution of the equality.
why it matters
This injectivity lemma is invoked by add_event_balanced_list to preserve the balanced_list predicate when an event and its reciprocal are adjoined, and by conservation_from_balance to derive zero net flow from the balanced condition. It supplies a required step in the module's derivation of double-entry structure from J-symmetry. Within the Recognition Science chain it reinforces the discrete event algebra that supports the eight-tick octave and spatial dimension forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.