Jcost_zero_iff_one
plain-language theorem explainer
The lemma establishes that the J-cost function vanishes only at unity for positive real arguments. Researchers on graph rigidity and energy balances in Recognition Science cite this uniqueness when showing that zero-cost configurations force constant fields. The proof is a one-line term application of the biconditional equivalence already established for the same cost function.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. If $J(x) = 0$ and $x > 0$, then $x = 1$.
background
The J-cost function is defined as $J(x) = (x + x^{-1})/2 - 1$, equivalently written as cosh(log x) - 1. It is the cost on the multiplicative group of positive reals and obeys the Recognition Composition Law. The lemma resides in the Cost module and depends on the biconditional equivalence that states vanishing cost holds if and only if the argument equals one for positive x. Upstream structures include LedgerFactorization, which calibrates J on the positive reals, and PhiForcingDerived, which derives the functional form from the self-similar fixed point.
proof idea
The proof is a one-line term that applies the forward direction of the biconditional equivalence lemma for the cost function to the hypothesis that the cost vanishes.
why it matters
This uniqueness result supports the energy processing bridge theorem by ensuring that zero cost implies balance at unity. It also underpins ratio rigidity arguments in the graph rigidity paper, where vanishing edge costs force the field to be constant on connected components. The lemma instantiates the J-uniqueness step from the forcing chain T5 and closes the zero-location property needed for downstream applications in gravity and spectral emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.