jcost_ratio_zero_iff
plain-language theorem explainer
The declaration establishes that for positive reals v and n the J-cost of their ratio vanishes exactly when v equals n. Researchers citing the F1 foundation paper on log-domain geometry or multiplicative recognizer costs would invoke this equivalence when proving geometric-mean optimality for total bond cost. The proof is a one-line wrapper that reduces the ratio case to the base zero-iff-one lemma after confirming positivity of the argument.
Claim. For positive real numbers $v$ and $n$, the J-cost satisfies $J(v/n)=0$ if and only if $v=n$, where $J(x)=½(x+x^{-1})-1$.
background
The module develops log-domain J-cost geometry for the canonical reciprocal cost $J(x)=½(x+x^{-1})-1$. The J-cost function measures deviation from unity for positive ratios arising in multiplicative recognizers, while the cost of any recognition event is defined to be its J-cost. This result re-exports and specializes the upstream theorem F1.1.3 that $J(x)=0$ iff $x=1$ for $x>0$.
proof idea
The term proof first constructs the positivity witness $0<v/n$ from the given $0<v$ and $0<n$. It then rewrites the goal by direct application of the upstream lemma $Jcost(x)=0$ iff $x=1$. The final step invokes the standard division-equality fact $a/b=1$ iff $a=b$ when $b>0$.
why it matters
This supplies the F1.2.1 equivalence required by the foundation paper for totalJcost minimization at the geometric mean and for distinguishing simultaneous versus sequential descent. It anchors the J-cost identities used in frustrated-phase arguments for NS, P versus NP, and Yang-Mills. The result is fully proved and closes a direct link from the base zero-iff-one property to ratio comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.