Jcost_zero_iff_one
The lemma establishes that J-cost vanishes only at unity for positive reals. Researchers modeling energy balances or graph rigidity in Recognition Science invoke it to conclude uniformity from zero deviation. The argument is a direct one-line application of the forward direction of the biconditional Jcost_eq_zero_iff.
claimIf $x > 0$ and $J(x) = 0$, where $J(x) := (x + x^{-1})/2 - 1$, then $x = 1$.
background
Jcost is defined as Jcost x = (x + x^{-1})/2 - 1. It satisfies the Recognition Composition Law and is nonnegative with equality only at x=1. The Cost module develops its algebraic properties for use in forcing chains and physical models. The upstream lemma Jcost_eq_zero_iff supplies the full biconditional Jcost x = 0 ↔ x = 1 for x > 0, from which this one-direction result follows immediately.
proof idea
The proof is a one-line wrapper that applies the forward direction of Jcost_eq_zero_iff x hx to the hypothesis h.
why it matters in Recognition Science
This lemma feeds the energy_processing_bridge theorem, where zero cost implies balance, and the GraphRigidity results, where vanishing edge costs force constant fields on connected graphs. It encodes J-uniqueness from the T5 step of the forcing chain, ensuring the fixed point at unity propagates to rigidity and energy-processing statements.
scope and limits
- Does not apply when x ≤ 0.
- Does not prove the converse direction.
- Does not extend to complex numbers or other fields.
- Does not address asymptotic or approximate vanishing.
formal statement (Lean)
329lemma Jcost_zero_iff_one {x : ℝ} (hx : 0 < x) (h : Jcost x = 0) : x = 1 :=
proof body
Term-mode proof.
330 (Jcost_eq_zero_iff x hx).mp h
331
332/-! ## Triangle Inequality for J -/
333
334/-- J in terms of cosh: J(exp(t)) = cosh(t) - 1 -/