JcostL_unit0
plain-language theorem explainer
The reciprocal cost on recovered reals vanishes at the unit: J_L(1) = 0. Anyone working the LogicReal transport of the J-cost surface cites this as the base normalization. The proof is a short transport: equality is reduced via toReal to the already-proved real identity J(1) = 0.
Claim. On the recovered real line, the canonical reciprocal cost satisfies $J_L(1) = 0$, where $J_L(x) = (x + x^{-1})/2 - 1$ and $1$, $0$ are the images of the ordinary unit and zero under the Mathlib-to-LogicReal embedding.
background
The module is the transport mirror of the ordinary real J-cost core: definitions live on LogicReal (reals recovered from the logic foundation), and theorems are proved by reducing through toReal to the verified Mathlib-real surface.
The canonical reciprocal cost on recovered reals is $J_L(x) = (x + x^{-1})/2 - 1$. On ordinary reals the same formula is $J(x)$, and the base fact $J(1) = 0$ is already recorded as a one-line simplification. Equality of recovered reals is equivalent to equality after transport: $x = y$ iff $\mathrm{toReal}(x) = \mathrm{toReal}(y)$. The embedding fromReal is a section of toReal.
In the Recognition Science forcing chain this $J$ is the unique cost fixed by T5 (equivalently $\cosh(\log x) - 1$), and the unit-normalization $J(1) = 0$ is the first algebraic checkpoint before symmetry, nonnegativity, and the composition law.
proof idea
Term-mode transport wrapper. Rewrite the goal with equality-transfer (eq_iff_toReal_eq), so it becomes an equality of ordinary reals. Simplify the left side by toReal_JcostL (which says $\mathrm{toReal}(J_L(x)) = J(\mathrm{toReal}(x))$) and both sides by toReal_fromReal (which cancels the embedding). The residual goal is exactly Jcost_unit0: $J(1) = 0$.
why it matters
Closes the unit-normalization step on the LogicReal cost surface so later lemmas can treat $J_L$ as a genuine cost rather than a formal expression. Immediate parent is JcostL_zero_iff, which upgrades this point evaluation to the characterization "$J_L(x) = 0$ iff $x = 1$" for positive recovered reals; that characterization is the zero-locus half of T5 uniqueness on the transported line.
Downstream the same transport pattern (reduce by toReal, quote the real theorem) is reused for symmetry, nonnegativity, the squared-ratio form, and the Recognition Composition Law on LogicReal. Framework landmark: T5 J-uniqueness and the RCL identity both presuppose $J(1) = 0$ as the neutral value of the cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.