eq_self_or_inv
Any J-automorphism of the positive reals maps each point to itself or its reciprocal. Researchers classifying the automorphism group of the canonical cost algebra cite this when reducing global statements to pointwise choices. The proof is a direct term reduction that applies cost preservation to reach the level-set lemma J_eq_iff_eq_or_inv and lifts via subtype extensionality.
claimLet $f$ be a J-automorphism of the positive reals and let $x>0$. Then $f(x)=x$ or $f(x)=x^{-1}$.
background
J is the cost function $J(x)=½(x+x^{-1})-1$ on positive reals, the unique solution to the Recognition Composition Law. PosReal is the subtype {x:ℝ // 0<x}. JAut consists of multiplicative maps PosReal→PosReal that also preserve J-values. The key upstream lemma J_eq_iff_eq_or_inv states that J y = J x on positive reals if and only if y=x or y=x^{-1}. preserves_cost extracts the J-preservation property from the JAut definition.
proof idea
Apply preserves_cost to obtain J((f x).1)=J(x.1). Feed this into J_eq_iff_eq_or_inv to split into the two cases at the level of underlying reals. In each branch apply Subtype.ext to recover the PosReal equality.
why it matters in Recognition Science
This supplies the pointwise disjunction used by eq_id_or_reciprocal to conclude that every J-automorphism is either the identity or the reciprocal map, and by eq_id_of_map_two_eq_two to force the identity when 2 is fixed. It completes the local analysis of symmetries in the cost algebra and supports the J-uniqueness step (T5) in the forcing chain by restricting admissible automorphisms.
scope and limits
- Does not prove existence of any J-automorphism beyond the identity and reciprocal.
- Does not apply to zero or negative reals.
- Does not impose or use continuity or measurability on f.
- Does not classify automorphisms under extra fixed-point assumptions.
Lean usage
rcases eq_self_or_inv f x with hfx | hfxformal statement (Lean)
836theorem eq_self_or_inv (f : JAut) (x : PosReal) :
837 f x = x ∨ f x = posInv x := by
proof body
Term-mode proof.
838 have hJ : J (f x).1 = J x.1 := f.preserves_cost x
839 rcases (J_eq_iff_eq_or_inv x.2 (f x).2).mp hJ with h | h
840 · left
841 exact Subtype.ext h
842 · right
843 exact Subtype.ext h
844
845/-- If `2 * x⁻¹ = 2 * x`, positivity forces `x = 1`. -/