paired_log_sum_zero
plain-language theorem explainer
The theorem shows that for any recognition event e the sum of the logarithm of its ratio and the logarithm of the ratio of its reciprocal event equals zero. Researchers deriving conservation from J-symmetry in ledger structures cite this step when closing the double-entry argument. The proof is a one-line wrapper that unfolds the reciprocal definition and invokes the log cancellation lemma on the positive ratio.
Claim. Let $e$ be a recognition event with positive ratio $r$. Then $log r + log(1/r) = 0$, where $1/r$ is the ratio of the reciprocal event obtained by swapping source and target agents.
background
RecognitionEvent is the structure with fields source and target (natural numbers), ratio (positive real), and ratio_pos (proof of positivity). The reciprocal operation on an event swaps source with target and replaces the ratio by its multiplicative inverse while preserving positivity. The module LedgerForcing derives double-entry ledger structure from J-symmetry in the cost algebra. The upstream lemma log_reciprocal_cancel states that for any positive real $r$, $log r + log(1/r) = 0$, obtained by rewriting the logarithm of the inverse and applying ring arithmetic.
proof idea
The proof is a one-line wrapper. It simplifies the reciprocal definition to expose the inverse ratio, then applies the lemma log_reciprocal_cancel directly to the positivity witness of the event ratio.
why it matters
This result supplies the third conjunct of the ledger_forcing_principle theorem, which states that J-symmetry implies paired reciprocal events, equal costs, log-ratio cancellation, and the existence of a balanced ledger with zero cost. It closes the conservation link required by the double-entry structure forced from the J-automorphism, consistent with the module's derivation of bookkeeping from symmetry. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.