reciprocal_comp_reciprocal
plain-language theorem explainer
The reciprocal J-automorphism on positive reals is an involution: its composition with itself recovers the identity map. Researchers verifying the structure of the cost algebra's automorphism group would cite this to confirm that the reciprocal branch closes under two applications. The proof is a one-line wrapper that invokes the extensionality lemma for JAut and reduces via simplification of the composition, reciprocal, and identity definitions.
Claim. Let $r$ be the reciprocal automorphism of the positive reals (sending each $x$ to its multiplicative inverse while preserving the $J$-cost). Then the composition $r \circ r$ equals the identity automorphism.
background
JAut is the type of honest automorphisms of the canonical cost algebra on positive reals: maps $f : \mathbb{R}{>0} \to \mathbb{R}{>0}$ that preserve the multiplicative operation posMul and satisfy $J(f(x)) = J(x)$ for the cost function $J$. The operation comp composes two such maps while preserving the automorphism properties. The identity element id is the map that fixes every positive real. The reciprocal map is the noncomputable automorphism sending each positive real to its multiplicative inverse via posInv, which satisfies the preservation conditions by direct verification of the multiplicative and $J$-invariance axioms.
proof idea
The proof applies the extensionality lemma JAut.ext to reduce equality of automorphisms to pointwise agreement on positive reals. It then invokes simp on the definitions of comp (function composition), reciprocal (posInv), and id (the identity function), which immediately yields the required equality.
why it matters
This result closes the involution property for the reciprocal branch inside the cost algebra, a basic algebraic fact needed to classify the honest automorphisms that preserve both multiplication and the $J$-cost. It sits among the sibling lemmas that establish the algebra structure (J, J_reciprocal, SatisfiesRCL) and supports the Recognition Composition Law by confirming that the two admissible branches (identity and reciprocal) behave as expected under composition. No downstream uses are recorded, indicating it functions as an internal closure fact rather than a direct input to higher theorems in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.