posInv
plain-language theorem explainer
The reciprocal map on positive reals sends each element to its multiplicative inverse while preserving positivity. Researchers classifying the automorphisms of the J-cost algebra cite it when proving that every continuous multiplicative bijection preserving J is either the identity or this reciprocal. The definition constructs it directly from the real inverse together with the positivity preservation fact.
Claim. Let $x > 0$ be a positive real. The reciprocal map sends $x$ to $x^{-1}$, which remains positive.
background
PosReal is the subtype of real numbers strictly greater than zero, serving as the genuine positive domain of the canonical cost algebra. The J functional on this domain is given by $J(x) = (x + x^{-1})/2 - 1$, satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This definition sits in the CostAlgebra module, which supplies the algebraic operations needed for the automorphism classification that follows the J-uniqueness step.
proof idea
The definition is a direct subtype constructor that applies the real inverse to the underlying value and invokes the inverse-positivity lemma to confirm the result stays in PosReal.
why it matters
This reciprocal map supplies the second branch in the classification that every J-automorphism is either the identity or the reciprocal. It is invoked by the theorems eq_id_or_reciprocal and continuous_bijective_preserves_J_eq_id_or_inv, which close the automorphism analysis feeding the T5 J-uniqueness landmark in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.