two_mul_inv_ne_inv_two_mul
plain-language theorem explainer
The theorem shows that 2 times the reciprocal of a positive real never equals the reciprocal of twice that real. Automorphism arguments in the cost algebra cite it to block any map that would interchange scaling by 2 with inversion. The short tactic proof assumes the equality, coerces to the underlying reals, clears denominators with field_simp, and obtains an immediate numerical contradiction.
Claim. For every positive real number $x$, $2x^{-1}neq(2x)^{-1}$.
background
PosReal is the subtype of strictly positive reals. posMul and posInv are the multiplication and inversion operations induced on this subtype, while posTwo is the constant element 2. The lemma lives in the CostAlgebra module that supplies the algebraic operations required by the J-cost function and the Recognition Composition Law. It draws on the concrete definitions of posInv and posMul supplied in the same file together with the identity event from ObserverForcing that places the cost minimum at 1.
proof idea
The proof assumes the contrary equality h, extracts the corresponding real equality via congrArg Subtype.val, records that x is nonzero by ne_of_gt, then applies field_simp to clear the denominators and norm_num to reach a contradiction.
why it matters
The result is invoked inside eq_id_of_map_two_eq_two to conclude that any J-automorphism fixing 2 must be the identity map. It therefore supports the uniqueness claim for the J-cost function (T5 of the forcing chain) by excluding nontrivial automorphisms that preserve the distinguished element 2. In the Recognition Science setting it closes one algebraic step needed to establish that the only structure-preserving map on the positive reals is the identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.