posInv_two
plain-language theorem explainer
The theorem establishes that the multiplicative inverse of the distinguished positive real 2 equals the distinguished positive real 1/2. Researchers working on the Recognition Science cost algebra would cite this when simplifying expressions involving inverses of small integers in proofs of the Recognition Composition Law. The proof proceeds by a direct application of subtype extensionality followed by numerical normalization on the underlying real numbers.
Claim. Let $x$ be a positive real. Let $i(x)$ denote its multiplicative inverse. Then $i(2) = 1/2$.
background
In the CostAlgebra module, positive reals form a subtype of the reals equipped with an explicit positivity witness. The inversion operation maps a positive real $x$ to its reciprocal, preserving the positivity proof. The constants 2 and 1/2 are embedded as distinguished positive reals for use in closing automorphism arguments. This identity sits inside the algebra that supports the Recognition Composition Law and the J-cost functional equation.
proof idea
The proof is a one-line wrapper that applies Subtype.ext to reduce the equality of positive reals to an equality of underlying reals, then invokes norm_num on the definitions of inversion, the constant 2, and the constant 1/2.
why it matters
This identity closes the set of distinguished positive constants required for the automorphism proof referenced in the inversion definition. It supplies a concrete simplification step inside the algebra that underpins the Recognition Composition Law and the forcing chain from T0 to T8. No downstream uses are recorded yet, so the result functions as a basic closure lemma for later composition and defect calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.