eq_id_of_map_two_eq_two
plain-language theorem explainer
Any J-automorphism of the positive reals that fixes the distinguished element 2 must coincide with the identity map everywhere. Workers classifying the automorphism group of the cost algebra in Recognition Science cite this result to pin down the only two candidates. The proof applies the pointwise identity-or-reciprocal dichotomy and obtains a contradiction on the reciprocal branch by multiplying against the fixed 2 and invoking the multiplicative property.
Claim. Let $f$ be a $J$-automorphism of the positive reals (i.e., a multiplicative map that also preserves the $J$-cost function). If $f(2)=2$, then $f$ is the identity map.
background
JAut consists of maps from positive reals to positive reals that are multiplicative under posMul and satisfy J(f(x)) = J(x) for the cost function J. The element posTwo is the distinguished positive real 2. The identity automorphism id is the obvious map that sends every positive real to itself. Upstream, eq_self_or_inv establishes that any such f acts pointwise either as the identity or as the reciprocal map posInv on each input.
proof idea
Apply JAut.ext to reduce to pointwise equality. For arbitrary x invoke eq_self_or_inv to split into the identity case (immediate) or the reciprocal case. In the latter branch form the product 2·x, apply multiplicativity to obtain f(2·x) = 2·(1/x), then split again on eq_self_or_inv for that product. The identity subcase forces x=1 and yields a contradiction with the reciprocal assumption via two_mul_inv_eq_two_mul_iff; the remaining subcase is ruled out by two_mul_inv_ne_inv_two_mul.
why it matters
This lemma supplies the missing case that lets eq_id_or_reciprocal conclude every J-automorphism is either the identity or the reciprocal map. It therefore closes the classification of honest automorphisms of the cost algebra, a prerequisite for the Recognition Composition Law and for the uniqueness statements that appear later in the forcing chain (T5 J-uniqueness).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.