reciprocal_comp_reciprocal
plain-language theorem explainer
The reciprocal J-automorphism composed with itself equals the identity automorphism on positive reals. Algebraists verifying the involution property of the reciprocal branch in the cost algebra would cite this result. The proof applies the extensionality lemma for J-automorphisms followed by direct simplification of the composition and inversion definitions.
Claim. Let $f$ denote the reciprocal automorphism of the canonical cost algebra on positive reals (the map $x \mapsto x^{-1}$ that preserves multiplication and the function $J$). Then $f \circ f$ equals the identity automorphism.
background
JAut consists of maps from positive reals to positive reals that preserve the multiplicative operation posMul and satisfy $J(f(x)) = J(x)$ for the cost function $J(x) = (x + x^{-1})/2 - 1$. The operation comp forms the composition of two such maps while preserving the automorphism properties. The reciprocal map is defined via posInv and shown to be a JAut element. The identity map is the obvious fixed-point automorphism. These sit inside the CostAlgebra module that equips positive reals with the Recognition Composition Law structure.
proof idea
One-line wrapper that applies the JAut extensionality lemma to reduce equality of automorphisms to pointwise agreement, then invokes simp on the definitions of comp, reciprocal, and id to obtain the identity function.
why it matters
This establishes that the reciprocal branch is an involution, directly supporting the module comment that any J-automorphism is pointwise either the identity or the reciprocal. It supplies a basic algebraic fact used in proofs involving the two possible branches under J-uniqueness (T5). The result belongs to the algebra layer that underpins the Recognition Composition Law and the forcing chain from T0 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.