pith. machine review for the scientific record. sign in
def definition def or abbrev high

reciprocal

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  48noncomputable def reciprocal (e : RecognitionEvent) : RecognitionEvent := {

proof body

Definition body.

  49  source := e.target
  50  target := e.source
  51  ratio := e.ratio⁻¹
  52  ratio_pos := inv_pos.mpr e.ratio_pos
  53}
  54
  55/-- The reciprocal of a reciprocal is the original event. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (13)

Lean names referenced from this declaration's body.