J_eq_iff_eq_or_inv
plain-language theorem explainer
The theorem classifies the level sets of the J-cost function on positive reals: J(y) equals J(x) precisely when y equals x or the reciprocal of x. Algebraists working on automorphisms of the cost structure cite this when restricting J-preserving maps to the identity and inversion branches. The proof reduces J(y) = J(x) to the factored equation (y - x)(x y - 1) = 0 by clearing denominators, then splits cases via the zero-product property and invokes J_reciprocal on the converse.
Claim. For positive real numbers $x$ and $y$, the J-cost satisfies $J(y) = J(x)$ if and only if $y = x$ or $y = x^{-1}$.
background
The J-cost function is defined by $J(x) = ½(x + x^{-1}) - 1$ on positive reals; it is the unique function satisfying the Recognition Composition Law. The CostAlgebra module develops its algebraic properties, including symmetry under inversion. Upstream, J_reciprocal states that cost is invariant under inversion, encoding the double-entry symmetry of the framework. The proof also draws on mul_eq_zero from the integers foundation and basic field simplifications.
proof idea
The forward direction unfolds J to obtain y + y^{-1} = x + x^{-1}, clears denominators via field_simp, and factors the difference as (y - x)(x y - 1) = 0 by ring. mul_eq_zero splits into the two cases, each solved by linarith. The converse applies rfl to the identity branch and J_reciprocal to the inversion branch.
why it matters
This result feeds eq_self_or_inv, which concludes that any J-automorphism on positive reals selects only the identity or reciprocal branch. It supplies the level-set classification step required for the algebraic structure of the cost function, consistent with J-uniqueness in the forcing chain. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.