posInv_inv
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.