Jcost_eq_sq
plain-language theorem explainer
The J-cost admits the equivalent squared-ratio form (x-1)^2/(2x) for every nonzero real x. Aesthetics and cosmology modules cite the identity to obtain monotonicity on (0,1] and explicit threshold bands at phi. The derivation is a one-line wrapper that unfolds the definition, clears the denominator with field_simp, and normalizes with ring.
Claim. For every real $x$ with $x ≠ 0$, $J(x) = (x-1)^2 / (2x)$, where the J-cost is given by $J(x) := (x + x^{-1})/2 - 1$.
background
The Cost module defines Jcost x := (x + x^{-1})/2 - 1, the functional form fixed by J-uniqueness in the forcing chain. This expression is the starting point for all cost calculations in Recognition Science and is algebraically equivalent to cosh(log x) - 1 on the positive reals. The present lemma rewrites it as a squared deviation that simplifies sign checks and monotonicity arguments.
proof idea
The proof unfolds the definition of Jcost, invokes field_simp under the hypothesis x ≠ 0 to clear the denominator, and finishes with ring to obtain the squared form.
why it matters
Downstream theorems such as Jcost_anti_mono_on_unit_interval and wallpaperJ_pos_of_ne_one invoke the squared form to prove that J-cost decreases toward unity and is strictly positive away from it. J_defect_form quotes the identity verbatim as the defect characterization, while predictability_threshold_band and Jcost_phi_val use it to evaluate the band around phi. The lemma therefore supplies the algebraic bridge between the primitive J-uniqueness (T5) and the Recognition Composition Law applications that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Multidimensional cost geometry
"1 + β u^T A⁻¹ u = 1 − coth(S)Σαᵢ, so singular hypersurface is tanh(S) = Σαᵢ when |Σαᵢ| < 1."