reciprocal
plain-language theorem explainer
The reciprocal definition constructs the inverse recognition event by swapping source and target while inverting the ratio. Researchers deriving double-entry ledger structure from J-symmetry cite it when classifying automorphisms of the cost algebra. Construction proceeds by direct field assignment that inherits positivity from the multiplicative inverse on positive reals.
Claim. Let $e$ be a recognition event with source $A$, target $B$, and positive ratio $r$. The reciprocal event has source $B$, target $A$, and ratio $r^{-1}$.
background
RecognitionEvent is the structure that records a directed recognition between two agents via natural-number source and target together with a positive real ratio. The LedgerForcing module shows that J-symmetry on costs forces double-entry ledger structure. Upstream, the reciprocal in CostAlgebra is the automorphism that inverts positive reals while preserving the J functional.
proof idea
Direct definition that swaps source and target, replaces the ratio by its multiplicative inverse, and discharges the positivity obligation via inv_pos.mpr applied to the input hypothesis.
why it matters
This definition supplies the reciprocal map used to classify J-automorphisms in CostAlgebra, including the theorem that every such automorphism is either the identity or the reciprocal. It underpins reciprocal symmetry in aesthetic cost models, where the Berlyne inverted-U appears as the RS reciprocal-symmetry signature. It fills the ledger-forcing step from J-symmetry to double-entry accounting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.