two_mul_inv_eq_two_mul_iff
plain-language theorem explainer
The equivalence asserts that on positive reals, twice the reciprocal equals twice the number precisely when the number equals one. Algebraists deriving fixed-point uniqueness in the cost algebra cite this to close scaling arguments. The proof reduces the equality via field simplification on the underlying reals, then applies linear arithmetic to extract the unit value from the resulting quadratic.
Claim. For $x > 0$, $2 x^{-1} = 2 x$ if and only if $x = 1$.
background
PosReal is the subtype of positive reals. posMul and posInv supply multiplication and inversion inside this domain; posTwo and posOne are the constants 2 and 1. The lemma lives in the CostAlgebra module that equips the positive reals with the structure needed for the Recognition Composition Law and J-cost functions. It draws on the basic operations posInv and posMul together with the positivity axioms to manipulate scaled equations.
proof idea
Constructor splits the biconditional. The forward direction applies Subtype.ext, extracts the real-valued equality, invokes field_simp with the nonzeroness fact, then uses linarith to obtain $x^2 = 1$ followed by nlinarith to conclude $x = 1$. The reverse direction substitutes the hypothesis and simplifies directly with the definitions of posMul, posInv, posOne and posTwo.
why it matters
The result is invoked by eq_id_of_map_two_eq_two, which proves that any automorphism fixing 2 is the identity map. It therefore supports the uniqueness of the J-automorphism in the cost algebra, a step that feeds the forcing chain from the functional equation to the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.