Jlog_eq_zero_iff
plain-language theorem explainer
The lemma establishes that the log-domain J-cost vanishes precisely when its argument is zero. Researchers reducing zero-cost conditions in multiplicative or log-coordinate settings would cite this equivalence when simplifying balance-point arguments. The proof splits the biconditional via constructor, derives a contradiction from the positivity lemma on the forward direction, and substitutes directly on the converse.
Claim. For every real number $t$, $J(t) = 0$ if and only if $t = 0$, where $J(t) = (e^t + e^{-t})/2 - 1$.
background
Jlog is defined in the Cost.Jlog module as the explicit hyperbolic expression $Jlog t := ((Real.exp t + Real.exp (-t))/2) - 1$, equivalently cosh(t) - 1. This measures multiplicative deviation from the unit element in log coordinates. The module develops its basic analytic properties, including non-negativity and strict monotonicity on the non-negative reals.
proof idea
The term-mode proof opens with constructor to split the biconditional. The forward direction assumes Jlog t = 0 together with t ≠ 0, invokes Jlog_pos_iff to obtain the strict inequality 0 < Jlog t, and closes by linarith. The reverse direction substitutes t = 0 and applies simp on the definition of Jlog.
why it matters
This zero-characterization lemma is invoked by JcostN_eq_zero_iff in Ndim.Core to reduce higher-dimensional cost vanishing to a dot-product condition on log vectors, and by jcost_log_zero_unique in PrimeLedgerStructure to identify the unique real zero of the J-cost at the RS balance point x = 1. It also supports Flog_eq_zero_iff_of_derivation when lifting the result through averaging derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.