log_reciprocal_cancel
plain-language theorem explainer
Log reciprocal cancellation establishes that for positive real r the sum of log r and log of its reciprocal is zero. Researchers deriving double-entry ledger structure from J-symmetry in Recognition Science cite it to obtain net-zero logarithmic contributions between paired events. The proof is a one-line wrapper that rewrites the inverse logarithm and normalizes the ring expression.
Claim. For any positive real number $r$, $log r + log(r^{-1}) = 0$.
background
The LedgerForcing module proves that J-symmetry forces double-entry ledger structure. The reciprocal of a RecognitionEvent swaps source and target while inverting the ratio, supplying the inverse automorphism on positive reals. This supplies the logarithmic identity required to show that paired events cancel in net flow and net log contribution.
proof idea
The proof is a one-line wrapper. It rewrites Real.log(r^{-1}) via the standard logarithm inverse rule, then applies ring normalization to reach zero.
why it matters
This identity is invoked by paired_log_sum_zero to prove that logs of an event and its reciprocal sum to zero, and by flow_contribution_reciprocal to establish negated flow contributions. It supplies the algebraic step inside the LedgerForcing chain from J-symmetry to double-entry bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.