J_symmetric
plain-language theorem explainer
The cost functional J satisfies J(x) = J(1/x) for every nonzero real x. Ledger forcing derivations and recognition event pairings cite this symmetry to obtain paired costs and conservation. The proof is a one-line term reduction that substitutes the definition of J and applies the ring tactic after canceling the double inverse.
Claim. For every real number $x ≠ 0$, $J(x) = J(x^{-1})$, where $J(y) := (y + y^{-1})/2 - 1$.
background
J is the cost functional defined by $J(x) = (x + x^{-1})/2 - 1$. The LedgerForcing module proves that J-symmetry forces double-entry ledger structure. Upstream statements in CostAxioms and HiggsMechanism establish the identical identity under the extra hypothesis that x is positive.
proof idea
The proof is a term-mode one-liner. It applies simp only [J, inv_inv] to unfold the definition and replace the inverse of the inverse, then invokes the ring tactic to confirm the algebraic identity.
why it matters
This symmetry supplies the first conjunct of the ledger_forcing_principle, which chains J-symmetry through paired recognition events to log-sum cancellation and the existence of a balanced ledger. It occupies the J-symmetry position in the forcing chain from d'Alembert uniqueness to double-entry bookkeeping and appears in multiple modules as a foundational identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Clipping a single ratio replaces the trust region in policy gradients
"L^CLIP is asymmetric: for Â_t > 0 the clip activates only when r_t > 1+ε; for Â_t < 0 only when r_t < 1−ε. The objective is not invariant under r ↦ 1/r."