Jcost_eq_sq
plain-language theorem explainer
The lemma gives the explicit algebraic form of the J-cost: for nonzero real x, J(x) equals (x minus 1) squared over 2x. Analysts of symmetry groups and threshold phenomena in Recognition Science invoke this identity to simplify monotonicity and positivity arguments. The proof clears the denominator by multiplying through by 2x, confirms both sides match via field simplification and ring, then cancels the nonzero factor.
Claim. For all real numbers $x ≠ 0$, if $J(x) := (x + x^{-1})/2 - 1$, then $J(x) = (x-1)^2 / (2x)$.
background
The J-cost is defined as $J(x) = (x + x^{-1})/2 - 1$. This expression measures the recognition cost of a ratio x away from unity and appears throughout the cost domain. The lemma lives in the JcostCore submodule and supplies the squared-ratio form required for defect characterizations and numerical bands. Upstream results establish the basic unfolding of the definition that leads directly to this identity.
proof idea
The tactic proof first records that 2x is nonzero. It then multiplies both sides by 2x, unfolds the definition of Jcost on the left, and verifies equality to (x-1)^2 using field_simp and ring. The same cancellation holds for the target right-hand side. Multiplication cancellation on the common nonzero factor finishes the argument.
why it matters
This supplies the operational expression for J(x) that all cost-based arguments rely upon. It is invoked in proofs of J-cost anti-monotonicity on the unit interval, strict positivity away from unity for wallpaper symmetries, defect forms in the algebra, and the numerical bands for predictability and ignition thresholds. Within the framework it realizes the explicit form of the J-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.