Jcost_symm
plain-language theorem explainer
The lemma shows that J-cost is unchanged when its argument is replaced by its reciprocal for any positive real. Modelers in acoustics, aesthetics, and chemistry cite it to establish symmetry of penalties around unity ratio. The short proof rewrites both sides using the squared form of J-cost and verifies the identity by simplification.
Claim. For every positive real number $x$, $J(x) = J(x^{-1})$, where $J(x) = (x + x^{-1})/2 - 1$.
background
J-cost is defined by the expression $J(x) = (x + x^{-1})/2 - 1$. This is the unique function satisfying the composition law in the Recognition framework. The equivalent squared-ratio form $J(x) = (x-1)^2/(2x)$ for nonzero $x$ is given by the lemma Jcost_eq_sq.
proof idea
The proof derives that $x$ is nonzero from the strict positivity assumption. It substitutes the squared-ratio expression for J-cost on both $x$ and its inverse. Field simplification removes denominators, after which the ring tactic confirms the two sides are identical.
why it matters
This lemma is used in dozens of applications, such as establishing symmetric pleasure in the Berlyne model and reciprocal cost in speech intelligibility. It encodes the double-entry property for ratios, aligning with the J-uniqueness at T5 of the forcing chain. The result closes the algebraic symmetry needed for the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 5 of 5)
-
RL reasoning performance saturates as policy entropy drops to zero
"the change in policy entropy is driven by the covariance between action probability and the change in logits, which is proportional to its advantage"
-
Lattice Weyl fermion gets an exact chiral symmetry, no doubling
"finite-range non-on-site chiral symmetry ... S_chiral(k) = ½[(1+cos k_z) τ^z + sin k_z τ^x]"
-
Point-free relations recovered from a parallel pair of frame operators
"A pair of cones △, ▽ : L → L on a meet-semilattice is called parallel if for all x,y ∈ L: △x ∧ y ⊑ △(x ∧ ▽y) and x ∧ ▽y ⊑ ▽(△x ∧ y). … Note the resemblance of parallelness to the Frobenius reciprocity condition. … Conjugate pairs (Jónsson–Tarski 1951): △x ∧ y = ⊥ iff x ∧ ▽y = ⊥."
-
Golden-ratio exponent fixes a gravity kernel, then meets 147 galaxies
"Reciprocity J(x) = J(1/x) forces double-entry ledger structure"
-
Multidimensional cost geometry
"Symmetrized Itakura-Saito: ½(D_IS(1‖x) + D_IS(x‖1)) = J(x); Hessian metric in log coords is Fisher-Rao of normal family with mean m(S) = ∫₀^S √cosh u du."