jcost_eq_zero_iff
plain-language theorem explainer
J-cost vanishes for positive reals precisely at unity. F1 paper authors cite the result when they need the unique minimizer of the reciprocal cost. The argument rewrites via the squared-ratio identity, uses positivity to conclude the difference is zero, and recovers the unit case by substitution.
Claim. For every real number $x > 0$, $J(x) = 0$ if and only if $x = 1$, where $J(x) := 1/2 (x + x^{-1}) - 1$.
background
The module develops the log-domain geometry of the canonical reciprocal cost J(x) = 1/2 (x + x^{-1}) - 1. This cost serves as the basic deviation measure in multiplicative settings for the F1 foundation paper, which also treats geometric-mean optimality and simultaneous versus sequential descent.
proof idea
The forward direction assumes Jcost x = 0 with x > 0. It invokes the squared-form lemma Jcost_eq_sq to replace the cost by (x - 1)^2 / (2x). Positivity of the denominator then forces (x - 1)^2 = 0, hence x = 1. The converse direction substitutes x = 1 into the unit lemma Jcost_unit0.
why it matters
F1.1.3 supplies the uniqueness of the zero of J, which is invoked directly by the ratio form F1.2.1 (jcost_ratio_zero_iff) that equates vanishing cost on a ratio to equality of numerator and denominator. In the Recognition framework this pins the fixed point of the J map, consistent with T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.