Jlog_nonneg
plain-language theorem explainer
Jlog(t) is nonnegative for every real t. Researchers establishing global minima of the energy functional or nonnegativity of ledger posting costs cite this fact. The argument rewrites the expression via the hyperbolic cosine identity and applies the elementary bound cosh(t) >= 1.
Claim. $0 ≤ ((e^t + e^{-t})/2 - 1)$ for all real $t$, equivalently $0 ≤ cosh(t) - 1$.
background
Jlog is defined in the Cost.Jlog module by Jlog(t) := ((Real.exp t + Real.exp(-t))/2) - 1. The sibling lemma Jlog_eq_cosh_sub_one supplies the identity Jlog(t) = Real.cosh(t) - 1. In sibling modules Jlog is realized as Jcost composed with the exponential, so nonnegativity inherits from the base Jcost property on positive reals via AM-GM.
proof idea
The term proof rewrites the goal with Jlog_eq_cosh_sub_one to obtain 0 ≤ cosh(t) - 1, then applies sub_nonneg.mpr to the library fact Real.one_le_cosh t.
why it matters
This lemma is invoked in EL_global_min to establish that Jlog attains its global minimum at t = 0 and in ledgerJlogCost_nonneg to guarantee summed costs over ledger differences remain nonnegative. It supplies the elementary nonnegativity of the J-function required by the Recognition Science cost axioms and the forcing chain beginning at T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.