J_symmetric_ratio
plain-language theorem explainer
J-symmetry extends to ratios: for nonzero reals a and b the cost J satisfies J(a/b) = J(b/a). Modelers of recognition events in ledger systems cite this result to enforce balance without sign dependence. The argument rewrites the reciprocal of the ratio and applies the base symmetry theorem directly.
Claim. For nonzero real numbers $a, b$, $J(a/b) = J(b/a)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The cost functional is defined by $J(x) = (x + x^{-1})/2 - 1$ for real $x$. The module LedgerForcing shows that J-symmetry forces double-entry ledger structure. Upstream, J_symmetric establishes $J(x) = J(1/x)$ for $x ≠ 0$, with a version in CostAxioms requiring positivity.
proof idea
The proof first establishes that the reciprocal of a/b equals b/a by field simplification. It then invokes J_symmetric on the nonzero quotient a/b to conclude the equality.
why it matters
This result closes the ratio form of symmetry inside the ledger forcing chain, supporting double-entry accounting for recognition events. It builds on J_symmetric and feeds the structure for balanced lists and reciprocity in the same module. No open questions are flagged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.