JcostL_zero_iff
plain-language theorem explainer
On positive recovered reals, the reciprocal cost vanishes if and only if the argument is the unit. Anyone working the LogicReal transport of the J-cost uniqueness or composition law cites this kernel characterization. The proof pushes both directions through toReal, uses the squared form of real J-cost on the forward arrow, and the unit lemma on the reverse.
Claim. For every positive recovered real $x$, the canonical reciprocal cost satisfies $J_L(x) = 0$ if and only if $x = 1$, where $J_L(x) = (x + x^{-1})/2 - 1$ is valued in recovered reals.
background
The module JcostLogic is the transport mirror of the real J-cost core: definitions live on LogicReal (recovered reals), and theorems reduce to the already-verified real surface via toReal. The canonical reciprocal cost on recovered reals is
$$J_L(x) = \frac{x + x^{-1}}{2} - 1.$$
On ordinary reals the same formula is written $J(x) = (x + x^{-1})/2 - 1$, equivalently $J(x) = (x-1)^2/(2x)$ for $x \neq 0$. That squared identity is the algebraic engine behind zero-set statements: $J(x) = 0$ forces $x = 1$ on the positive ray. The unit evaluation $J_L(1) = 0$ is already recorded as a sibling lemma. In the broader Recognition framework this $J$ is the unique cost forced by the Recognition Composition Law (T5), so its zero locus is the unique fixed point of perfect match.
proof idea
Bidirectional constructor.
Forward: assume $J_L(x) = 0$. Equality of recovered reals is equivalent to equality after toReal. Positivity of $x$ transfers to positivity of toReal x, hence nonzero. Congruence under toReal plus the transport identity toReal (J_L x) = J(toReal x) yields $J(\mathrm{toReal}, x) = 0$. Rewrite via Jcost_eq_sq, clear the strictly positive denominator $2\cdot\mathrm{toReal}, x$, obtain $(\mathrm{toReal}, x - 1)^2 = 0$, hence $\mathrm{toReal}, x = 1$, and conclude $x = 1$.
Reverse: substitute $x = 1$ and apply the unit lemma $J_L(1) = 0$.
why it matters
This is the LogicReal form of the elementary fact that recognition cost vanishes only at perfect match. In the forcing chain, T5 identifies $J(x) = (x + x^{-1})/2 - 1$ as the unique cost obeying the Recognition Composition Law; the zero locus $J = 0 \Leftrightarrow x = 1$ is the uniqueness of the identity ratio. The module exists precisely so that later LogicReal arguments (composition law transport, nonnegativity, symmetry) can stay on recovered reals without dropping to ℝ at every step. No downstream consumers are wired yet in the graph, but the sibling suite (JcostL_nonneg, JcostL_symm, SatisfiesCompositionLawL, compositionLawL_to_real) is the natural home for any proof that needs "cost zero means unit" without leaving LogicReal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.