reciprocal_ne_id
plain-language theorem explainer
The reciprocal map on positive reals is shown to be a distinct J-automorphism from the identity map. Researchers classifying the automorphism group of the cost algebra cite this to confirm that Aut(J) has cardinality two. The proof assumes equality of the two maps, evaluates both at the distinguished point 2, and obtains the numerical contradiction 1/2 = 2 via congruence and norm_num.
Claim. Let $JAut$ be the group of maps $f : PosReal → PosReal$ that preserve multiplication and the $J$-cost function. Let $ι$ be the identity map and $ρ(x) = x^{-1}$ the reciprocal map. Then $ρ ≠ ι$ as elements of $JAut$.
background
JAut consists of maps on PosReal = {x : ℝ | 0 < x} that satisfy f(xy) = f(x)f(y) and J(f(x)) = J(x). The identity map id is the obvious inclusion x ↦ x. The reciprocal map is constructed via posInv(x) = x^{-1} and verified to lie in JAut by direct checking of the two preservation axioms. This theorem lives in the CostAlgebra module that equips the positive reals with the canonical cost structure underlying the Recognition Composition Law.
proof idea
The proof is by contradiction. Assume reciprocal = id. Congruence at the constant posTwo (the element 2) yields reciprocal(2) = id(2). Extracting the underlying real values and applying norm_num on the definitions of reciprocal, id, posInv and posTwo produces the equality 1/2 = 2, a contradiction.
why it matters
The result is invoked by equivFinTwo to build the explicit bijection JAut ≃ Fin 2 that sends id to 0 and reciprocal to 1. It therefore establishes that the automorphism group of the cost algebra consists exactly of these two elements, supplying the algebraic foundation for the two-point classification used in later Recognition Science arguments involving the J-function and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.