posInv_inv
Inversion on positive reals is an involution. Researchers formalizing the cost algebra cite this when reducing expressions that contain reciprocal costs in the Recognition Composition Law. The proof is a term-mode wrapper that applies subtype extensionality and simplifies directly on the definition of posInv.
claimFor every positive real number $x > 0$, if $iota(x) = x^{-1}$ denotes inversion, then $iota(iota(x)) = x$.
background
PosReal is the subtype of strictly positive reals. posInv is the map sending each such $x$ to its reciprocal while preserving positivity. The CostAlgebra module builds the algebraic structure on this domain that is compatible with the Recognition Composition Law and the J-cost functional equation.
proof idea
The proof is a one-line term wrapper. It applies Subtype.ext to reduce the equality of subtypes to an equality of underlying reals, then invokes simp on the definition of posInv to obtain the double-reciprocal identity.
why it matters in Recognition Science
This involution property supplies the basic simplification rule needed for expressions involving reciprocal costs. It supports the automorphism arguments that appear in the forcing chain at T5 (J-uniqueness) and T6 (phi fixed point). The declaration feeds no downstream results in the current graph.
scope and limits
- Does not extend the involution claim to zero or negative reals.
- Does not prove that inversion is the unique automorphism of the positive reals.
- Does not address the Recognition Composition Law or defectDist directly.
formal statement (Lean)
747@[simp] theorem posInv_inv (x : PosReal) : posInv (posInv x) = x := by
proof body
Term-mode proof.
748 apply Subtype.ext
749 simp [posInv]
750