Jlog_zero
plain-language theorem explainer
The lemma establishes that the log-domain recognition cost vanishes at the origin. Researchers deriving free-energy bounds or information-geometric equilibria cite this as the base case for global minimization. It follows from a one-line simplification that unfolds the definitions of Jlog and Jcost.
Claim. Let $Jlog(t) := Jcost(e^t)$ where $Jcost(x) = (x + x^{-1})/2 - 1$. Then $Jlog(0) = 0$.
background
In the Cost module the recognition cost is introduced as the function $Jcost(x) = (x + x^{-1})/2 - 1$ for $x > 0$, which is nonnegative by the AM-GM inequality (see Jcost_nonneg). The log-domain version is defined by $Jlog(t) := Jcost(e^t)$. The present lemma records the value at the natural origin $t = 0$, which corresponds to the unit scale $x = 1$ where the cost is minimized. Upstream, the definition of Jlog appears in both the main Cost module and the FlogEL and Jlog submodules.
proof idea
One-line wrapper that applies the simp tactic to the definitions of Jlog and Jcost, reducing the left-hand side directly to $(1 + 1)/2 - 1 = 0$.
why it matters
This base case is invoked by EL_global_min to establish that Jlog(0) is the global minimum and by Jlog_eq_zero_iff to characterize the zero set. It also supplies the first equality in the second-order equivalence between Jlog and the KL quadratic at equilibrium (see jcost_kl_same_second_order_at_equilibrium). Within the Recognition Science framework it anchors the T5 J-uniqueness property and the minimum of the phi-ladder at unit scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.