preserves_cost
plain-language theorem explainer
J-automorphisms of the positive reals preserve the J-cost function by definition. Researchers classifying automorphisms or building the cost algebra category cite this when verifying that compositions and morphisms remain cost-preserving. The proof is a one-line wrapper extracting the second component of the JAut subtype.
Claim. Let $f$ be a multiplicative map on positive reals that preserves the J-cost function, and let $x > 0$. Then $J(f(x)) = J(x)$.
background
The J-cost function is $J(x) = ½(x + x^{-1}) - 1$, the unique cost satisfying the Recognition Composition Law on positive reals. PosReal is the subtype of positive reals. JAut is the subtype of maps PosReal → PosReal that are multiplicative and satisfy J(f(x)) = J(x) for all x, as recorded in its definition.
proof idea
One-line wrapper that applies the second projection of the JAut subtype definition.
why it matters
This feeds the composition operation on JAut (comp) and the classification theorem eq_self_or_inv showing any such map is pointwise the identity or reciprocal. It underpins the CostMorphism structure in RecognitionCategory and anchors cost preservation in the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.