log_reciprocal_cancel
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend the identity to non-positive reals.
- Does not address complex or multi-valued logarithms.
- Does not derive the reciprocal event definition.
- Does not connect directly to phi-ladder mass formulas or T5-T8 forcing steps.
Lean usage
simp only [reciprocal]; exact log_reciprocal_cancel e.ratio_posformal statement (Lean)
126theorem log_reciprocal_cancel {r : ℝ} (_hr : r > 0) : Real.log r + Real.log (r⁻¹) = 0 := by
proof body
Term-mode proof.
127 rw [Real.log_inv]; ring
128
129/-- For any event e, logs of e and reciprocal(e) sum to zero. -/