posInv
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not extend inversion to zero or negative reals.
- Does not assert any preservation of J or the composition law.
- Does not provide numerical evaluation or approximation.
formal statement (Lean)
739noncomputable def posInv (x : PosReal) : PosReal :=
proof body
Definition body.
740 ⟨x.1⁻¹, inv_pos.mpr x.2⟩
741
742/-- Distinguished positive constants used to close the automorphism proof. -/