reciprocal_comp_reciprocal
The reciprocal J-automorphism squares to the identity on positive reals. Algebraists classifying maps that preserve both multiplication and the J-cost function would cite this when confirming the involution property inside JAut. The proof is a one-line wrapper that applies the JAut extensionality lemma and reduces the composition via the definitions of reciprocal and id.
claimLet $r$ denote the map $xmapsto x^{-1}$ on positive reals, which preserves multiplication and the J-cost. Then the composition of $r$ with itself equals the identity map: $rcirc r=mathrm{id}$.
background
JAut consists of maps from positive reals to positive reals that preserve the multiplicative operation posMul and satisfy J(f(x))=J(x). The comp operation on JAut is ordinary function composition, lifted so that the result remains a J-automorphism. The reciprocal is defined as the map sending each positive real to its multiplicative inverse and verified to lie in JAut. The identity is the obvious fixed map. This theorem appears in the CostAlgebra module that equips the canonical cost algebra with its automorphism group structure. The upstream comp definition records how composition is constructed while preserving the two JAut axioms; the reciprocal definition uses posInv together with mul_comm to check multiplicativity.
proof idea
The proof is a one-line wrapper that applies JAut.ext to reduce equality of automorphisms to pointwise equality on positive reals. It then introduces a variable x and invokes simp on the definitions of comp, reciprocal, and id, which unfolds the double inverse to the original element.
why it matters in Recognition Science
This result shows that the reciprocal branch is closed and of order two inside the automorphism group of the cost algebra. It directly supports the module comment that any J-automorphism is pointwise either the identity or the reciprocal. In the Recognition Science framework the fact aligns with T5 J-uniqueness and the self-similar fixed-point structure forced at T6, guaranteeing that the only involutive symmetry available is the one generated by inversion. It closes a basic algebraic relation needed before the Recognition Composition Law can be applied to composite costs.
scope and limits
- Does not classify all elements of JAut beyond the identity and reciprocal branches.
- Does not prove that JAut forms a group under comp.
- Does not connect the involution property to the Recognition Composition Law.
- Does not address continuity or measurability constraints on automorphisms.
formal statement (Lean)
829@[simp] theorem reciprocal_comp_reciprocal : comp reciprocal reciprocal = id := by
proof body
Term-mode proof.
830 apply JAut.ext
831 intro x
832 simp [comp, reciprocal, id]
833
834/-- Pointwise, a `J`-automorphism can only choose the identity branch or the
835 reciprocal branch. -/