Jlog_eq_zero_iff
The lemma establishes that the log-domain cost vanishes exactly when its argument is zero. Researchers working on multiplicative cost structures and log-coordinate formulations cite this equivalence to identify the unique balance point. The short term proof reduces the claim via simplification to the standard fact that the exponential equals one only at zero.
claimLet $J(t) := J(e^t)$ where $J$ is the cost function with $J(1)=0$. Then $J(t)=0$ if and only if $t=0$.
background
In the log-domain cost module the function Jlog is defined by composing the base cost with the exponential: Jlog(t) := Jcost(exp t). This places the cost in additive coordinates on the positive reals. The upstream lemma Jcost_unit0 states that Jcost(1)=0, which is the key algebraic fact used here. The module focuses on log-domain costs for derivations involving averaging functions.
proof idea
The term-mode proof applies simp with Jlog and Jcost_unit0 to reduce the statement to Real.exp t = 1 ↔ t = 0, then invokes the library fact Real.exp_eq_one_iff.
why it matters in Recognition Science
This lemma supports the zero-cost characterization in higher-dimensional and prime-ledger settings. It is invoked by Flog_eq_zero_iff_of_derivation and JcostN_eq_zero_iff to extend the uniqueness to derived cost functions and vector costs. In the Recognition framework it anchors the identification of the balance point x=1 in log coordinates, consistent with the J-uniqueness property.
scope and limits
- Does not prove that Jlog is nonnegative away from zero.
- Does not address differentiability or other analytic properties.
- Applies only to the real line with the standard exponential.
Lean usage
example (t : ℝ) : Jlog t = 0 ↔ t = 0 := Jlog_eq_zero_iff tformal statement (Lean)
10lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by
proof body
Term-mode proof.
11 simp [Jlog, Jcost_unit0]
12 have h : Real.exp t = 1 ↔ t = 0 := Real.exp_eq_one_iff
13 exact h
14