jcost_at_one
plain-language theorem explainer
The identity establishes that the reciprocal cost vanishes at the unit point. Workers on the F1 foundation paper and on geometric-mean minimization results cite this base case when normalizing energies or proving non-negativity. The proof is a direct one-line application of the core unit lemma.
Claim. $J(1) = 0$, where $J(x) = ½(x + x^{-1}) - 1$ for $x > 0$.
background
The module develops log-domain geometry for the canonical reciprocal cost in the F1 foundation paper. The cost is given by $J(x) = ½(x + x^{-1}) - 1$, equivalently expressed as the squared ratio $(x-1)^2/(2x)$. This supplies the zero point required for non-negativity and minimization statements listed in the module header.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module, which itself reduces by simplification on the definition of Jcost.
why it matters
The result occupies the F1.1.2 slot and anchors the non-negativity claim F1.1.3 together with geometric-mean optimality. It supplies the reference point for the J-cost identities used in the Recognition Science forcing chain and in the cited applications to NS, P vs NP, and Yang-Mills.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.