Jcost_symm
plain-language theorem explainer
Jcost_symm proves that the cost function satisfies Jcost(x) = Jcost(1/x) for every positive real x. Researchers in acoustics, aesthetics, and chemistry cite it to obtain reciprocal invariance in speech intelligibility, pleasure curves, and reaction thresholds. The tactic proof unfolds the definition, equates the two inner sums by field simplification and ring, then closes with simp.
Claim. For every real number $x > 0$, $Jcost(x) = Jcost(x^{-1})$, where $Jcost(x) := (x + x^{-1})/2 - 1$.
background
Jcost is defined by the expression (x + x^{-1})/2 - 1 on the reals. The Cost.JcostCore module collects the elementary algebraic properties of this function before it is specialized to particular domains. The lemma depends only on the definition together with the field axioms for the reals.
proof idea
Derive x nonzero from the positivity hypothesis. Unfold the definition of Jcost on both sides. Establish equality of the sums x + x^{-1} and x^{-1} + x by field_simp followed by ring. Finish with simp to obtain the desired equality.
why it matters
The lemma is invoked by forty downstream results, including pleasure_symmetric (aesthetics) and maillard_symmetric (chemistry). It supplies the algebraic content of reciprocal invariance required by the Recognition Composition Law and by the J-uniqueness step in the forcing chain. The result therefore closes the basic symmetry fact needed for all later cost-based models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.