posInv_one
plain-language theorem explainer
The identity shows that inversion on positive reals fixes the distinguished unit element. Workers verifying the automorphism group of the cost functional cite this fixed-point fact when checking preservation of constants. The proof is a one-line wrapper that reduces via subtype extensionality and simplifies directly on the explicit definitions of inversion and the unit.
Claim. Let $I$ denote inversion on positive reals and let $1$ be the unit element. Then $I(1) = 1$.
background
Positive reals carry the inversion map sending each element to its reciprocal while preserving positivity. The unit element is the real number one, packaged as a positive real. This identity belongs to the algebra layer of the cost functional, where the two distinguished constants are introduced precisely to close the automorphism argument.
proof idea
The proof applies subtype extensionality to reduce the claim to an equality of underlying reals, then simplifies using the definitions of inversion (reciprocal) and the unit (one).
why it matters
The result supplies one of the fixed-point checks needed to finish the automorphism proof for the cost functional. It aligns with the Recognition Composition Law by confirming that inversion respects the unit, consistent with the J-function and the overall forcing chain. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.