continuous_bijective_preserves_J_eq_id_or_inv
plain-language theorem explainer
Continuous multiplicative bijections on positive reals that preserve the J-cost must be the identity or the reciprocal map. Researchers classifying automorphisms of the cost algebra or closing uniqueness results for the Recognition Composition Law would cite this result. The proof constructs an element of the JAut type from the given hypotheses and applies the prior dichotomy theorem eq_id_or_reciprocal, then uses function extensionality to recover the explicit form of f.
Claim. Let $f : (0,∞) → (0,∞)$ be continuous and bijective with $f(xy) = f(x)f(y)$ for all $x,y > 0$ and $J(f(x)) = J(x)$ for all $x > 0$, where $J(x) = ½(x + x^{-1}) - 1$. Then either $f(x) = x$ for all $x > 0$ or $f(x) = x^{-1}$ for all $x > 0$.
background
J is the cost function defined by $J(x) = ½(x + x^{-1}) - 1$, the unique solution (modulo regularity) to the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. PosReal is the subtype of positive reals. JAut is the type of maps $f : PosReal → PosReal$ that are multiplicative with respect to posMul and preserve J-values. The shifted function H(x) = J(x) + 1 satisfies the d'Alembert equation. The upstream theorem eq_id_or_reciprocal states that every element of JAut is either the identity automorphism or the reciprocal automorphism.
proof idea
One-line wrapper that applies the classification theorem. The hypotheses are packaged into a term g of type JAut. Then rcases is used on eq_id_or_reciprocal g to obtain the two cases. Each case applies funext, followed by congrArg on the equality of automorphisms and simpa to recover that f equals the identity or the reciprocal map.
why it matters
This theorem supplies the continuous-bijective case of the automorphism classification that appears in the cost algebra certificate (items 9 and 10). It feeds the uniqueness step T5 of the forcing chain by showing that J-preserving multiplicative maps on the positive reals are exhausted by the identity and reciprocal. The result is cited by any downstream argument that needs to know the only regular automorphisms of the cost structure are these two involutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.