posInv_half
plain-language theorem explainer
Algebraists working on the positive reals cost structure cite this result when verifying that inversion preserves the distinguished constants one-half and two. The statement asserts that the inverse of the positive real one-half equals the positive real two. The proof reduces the claim to an equality of underlying reals and normalizes the explicit definitions.
Claim. The inversion map on positive reals sends the element one-half to the element two: if $x = 1/2$ then $x^{-1} = 2$.
background
In the CostAlgebra module the positive reals carry the inversion operation defined by taking the reciprocal of the underlying real while preserving positivity. The constants one-half and two are introduced as explicit subtype elements of PosReal via norm_num. This lemma belongs to the algebraic layer that prepares the canonical cost algebra on the positive reals for 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 to equality of the carrier reals, then invokes norm_num on the definitions of posInv, posTwo and posHalf.
why it matters
The result supplies a concrete case needed to close the honest automorphism type of the canonical cost algebra on the positive reals. It sits inside the algebraic foundation that supports the Recognition Composition Law and the J-uniqueness step of the forcing chain. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.