Jlog_nonneg
plain-language theorem explainer
Jlog(t) is nonnegative for every real t. Researchers on Recognition cost functions and ledger postings cite this to guarantee nonnegativity after logarithmic reparameterization. The proof is a one-line term wrapper applying Jcost_nonneg to the positive argument exp(t).
Claim. For every real number $t$, $0 ≤ J_{log}(t)$, where $J_{log}(t) := J(e^t)$ and $J(x) ≥ 0$ for all $x > 0$ by the AM-GM inequality.
background
Jlog is defined by composing the base cost function with the exponential: Jlog(t) = Jcost(exp(t)). This shifts the cost into the additive log-domain while preserving the nonnegativity property. The upstream Jcost_nonneg lemma states that J(x) ≥ 0 for x > 0, proved by rewriting Jcost(x) via its squared representation and applying positivity of squares and denominators. The Cost module uses this composition to support averaging derivations and ledger adjacency sums; the FlogEL sibling re-exports an identical definition for forcing-chain applications.
proof idea
The proof is a one-line term-mode wrapper: it supplies the hypothesis 0 < exp(t) from Real.exp_pos t directly to the Jcost_nonneg lemma.
why it matters
This lemma is invoked by EL_global_min to establish the global minimum at t = 0, by Flog_nonneg_of_derivation to transfer nonnegativity to averaging derivations, and by ledgerJlogCost_nonneg to bound posting costs. It closes the nonnegativity step required by the Recognition Composition Law and the T5 J-uniqueness in the forcing chain (T0-T8), ensuring costs remain nonnegative under the eight-tick octave reparameterization. It touches the open question of extending the phi-ladder mass formula to continuous log-domain costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.