J_defect_form
plain-language theorem explainer
Algebraists working with the Recognition Composition Law cite this result for the explicit defect form of the J-cost. It states that J(x) equals (x-1) squared over 2x for any nonzero real x. The proof is a direct one-line term application of the Jcost_eq_sq lemma that unfolds the definition and simplifies via field and ring tactics.
Claim. For every real number $x$ with $x$ nonzero, the J-cost function satisfies $J(x) = (x-1)^2 / (2x)$.
background
The J-cost is introduced in this module as the unique real-valued function satisfying the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y). It is defined by J(x) := Jcost(x), where the underlying Jcost satisfies the same functional equation and the normalization J(1) = 0. The local setting is the algebra of costs developed after the functional-equation axioms imported from Cost.FunctionalEquation and Cost.FunctionalEquationAczel. Upstream, the lemma Jcost_eq_sq already records the squared-ratio identity for Jcost itself.
proof idea
The proof is a one-line term wrapper that applies the lemma Jcost_eq_sq directly to the hypothesis hx : x ≠ 0. That lemma unfolds the definition of Jcost, invokes field_simp on the nonzero assumption, and finishes with ring normalization to obtain the defect expression.
why it matters
This supplies the closed algebraic form of the J-cost that appears throughout Recognition Science derivations, including the expression for G in RS-native units and the phi-ladder mass formula. It directly supports the J-uniqueness step (T5) of the forcing chain and the Recognition Composition Law itself. No downstream uses are recorded in the current graph, yet the form is presupposed by every cost-composition theorem in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.