Jlog_nonneg
plain-language theorem explainer
The lemma establishes nonnegativity of the log-domain cost Jlog(t) for every real t. Researchers bounding ledger posting costs or locating energy minima in Recognition Science models cite it to guarantee nonnegative totals. The proof reduces the claim to the AM-GM inequality on exp(t) and its reciprocal through a direct unfolding and calculation chain.
Claim. For every real number $t$, $0 ≤ J_{log}(t)$, where $J_{log}(t) := J(e^t)$ and $J(x) = (1/2)(x + x^{-1}) - 1$ for $x > 0$.
background
In the Cost.FlogEL module the log-domain cost is defined by composing the base cost Jcost with the exponential: Jlog(t) := Jcost(exp t). This converts the multiplicative J-structure into an additive function on the real line, supporting ledger and forcing calculations. The module imports the core Cost layer and sits alongside sibling definitions that sometimes rewrite the same object via cosh(t) - 1.
proof idea
The tactic proof first applies simp to unfold Jlog into Jcost(exp t). It then records positivity of exp(t) and invokes Real.add_ge_two_mul_sqrt to obtain exp(t) + exp(-t) ≥ 2. A short calc chain scales the inequality by 1/2, subtracts 1, and concludes the result is at least zero.
why it matters
The result feeds EL_global_min, which places the global minimum of Jlog at t = 0, and Flog_nonneg_of_derivation for averaging derivations. It also supports ledgerJlogCost_nonneg and postingStep theorems in LedgerPostingAdjacency. Within the framework it supplies the nonnegativity step required for J-uniqueness (T5) and for nonnegative costs on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.