Jlog_strictMonoOn_Ici0
plain-language theorem explainer
The function Jlog is strictly monotonic increasing on the closed interval from zero to infinity. Workers on cost ordering in the Recognition Science framework cite this to compare log-domain costs for positive arguments. The short proof reduces the claim to the strict increase of the hyperbolic cosine on that interval by rewriting Jlog as cosh minus one and subtracting one from both sides of the inequality.
Claim. The function $J(t) := (e^t + e^{-t})/2 - 1$ is strictly increasing on $[0, +infty)$.
background
In the Cost module the function Jlog is defined by Jlog(t) = (exp(t) + exp(-t))/2 - 1. This coincides with cosh(t) minus one, as shown by an upstream lemma that unfolds the definition and invokes the standard identity for the hyperbolic cosine. The module develops analytic properties of this cost function on the reals, resting on the reduction from seven axioms to four structural conditions plus three definitional facts.
proof idea
The proof opens by fixing x and y in the interval from zero to infinity with x less than y. It applies the strict monotonicity of cosh on that interval to obtain cosh(x) less than cosh(y). It then rewrites the goal using the identity Jlog(t) equals cosh(t) minus one on both sides and concludes with the fact that subtracting one preserves the strict inequality.
why it matters
This monotonicity is used in the downstream lemma that compares Jlog at one to Jlog at any x greater than one. It supplies an ordering property essential for the cost structure in Recognition Science, supporting comparisons that appear in the ledger adjacency relations. The result aligns with the J-uniqueness and the forcing chain steps that fix the form of the cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.