Jlog_zero
plain-language theorem explainer
The lemma establishes that the log-domain cost function evaluates to zero at the origin. Researchers in the Recognition Science cost framework cite this as the equilibrium base case for non-negativity and minimum properties. The proof is a one-line simplification that substitutes the explicit definition of Jlog.
Claim. Let $J(t) := (e^t + e^{-t})/2 - 1$. Then $J(0) = 0$.
background
In the Cost.Jlog module, Jlog is defined explicitly as the real function $Jlog(t) = (exp(t) + exp(-t))/2 - 1$, which is the log-domain form of Jcost. This matches the J-uniqueness expression from the forcing chain. Upstream results supply the equivalent definition Jlog(t) := Jcost(exp t) and the non-negativity lemma Jcost_nonneg for positive arguments.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of Jlog, reducing the expression at t=0 directly to zero.
why it matters
This lemma anchors the zero minimum of Jlog and feeds directly into EL_global_min and Jlog_eq_zero_iff. It supports the second-order equivalence with KL divergence in FEPBridgeFromJCost and aligns with the J-uniqueness step in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.