Jlog_eq_zero_iff
The equivalence shows that the logarithmic J-cost vanishes precisely when its argument is zero. Workers extending the cost function to vector spaces or prime structures cite this when reducing zero-cost conditions to the origin. The proof splits the biconditional, derives a contradiction from positivity on the nonzero side, and substitutes directly on the zero side.
claimLet $J(t) := (e^t + e^{-t})/2 - 1$. Then $J(t) = 0$ if and only if $t = 0$.
background
In the Cost.Jlog module, Jlog is defined explicitly as $(e^t + e^{-t})/2 - 1$, which equals cosh(t) minus one. This places the cost in additive log coordinates where multiplicative structures become additive. The result builds directly on the sibling positivity lemma Jlog_pos_iff, which states that Jlog is strictly positive away from zero, and on the definition of Jlog itself.
proof idea
The proof uses a constructor to split the biconditional. For the forward direction it assumes Jlog t equals zero but t nonzero, invokes Jlog_pos_iff to obtain 0 < Jlog t, and reaches a contradiction via linarith. For the reverse direction it substitutes t equals zero and simplifies the definition of Jlog to zero.
why it matters in Recognition Science
This lemma supplies the zero characterization needed for higher-dimensional extensions such as JcostN_eq_zero_iff in the Ndim module and for Flog_eq_zero_iff_of_derivation in the FlogEL development. It also anchors the uniqueness result jcost_log_zero_unique in the prime ledger structure, confirming that the balance point x equals one corresponds to t equals zero in log space. Within the Recognition framework this pins the unique minimum of the J-cost at the identity element.
scope and limits
- Does not extend the equivalence to complex arguments.
- Does not quantify the growth rate of Jlog away from zero.
- Does not address discrete or integer-restricted domains.
Lean usage
simpa [Jlog] using (Jlog_eq_zero_iff (t := dot α (logVec x)))formal statement (Lean)
40@[simp] lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by
proof body
Term-mode proof.
41 constructor
42 · intro ht
43 by_contra hne
44 have : 0 < Jlog t := (Jlog_pos_iff t).2 hne
45 linarith
46 · intro ht
47 subst ht
48 simp [Jlog]
49