cosh_mul_monotoneOn
plain-language theorem explainer
For any real scale l ≥ 0, t ↦ cosh(l t) is nondecreasing on [0, ∞). Downstream, the order-route witness that the J-cost transform H(J) is monotone cites this at l = 1. The proof is a short term argument: reduce via cosh_le_cosh to absolute values, drop abs by nonnegativity of l·t on the ray, then scale the inequality by l.
Claim. Let $l \in \mathbb{R}$ with $l \ge 0$. Then the map $t \mapsto \cosh(l t)$ is nondecreasing on the closed ray $[0, \infty)$: if $0 \le a \le b$, then $\cosh(l a) \le \cosh(l b)$.
background
The module develops the monotone d'Alembert route in the Primitive Recognition Calculus: additive or multiplicative functional equations plus an order hypothesis force the cosh family, which is the analytic form of the Recognition cost.
Here the elementary comparison fact is isolated. Hyperbolic cosine is even and increasing on $[0,\infty)$, so on the nonnegative ray the composition $t \mapsto \cosh(l t)$ inherits monotonicity whenever the scale $l$ is nonnegative. The ambient cost side uses $J(x) = (x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ (T5 J-uniqueness), and the auxiliary transform $H$ that turns $J$ into a pure cosh profile on the additive line.
Sibling lemmas in the same file treat d'Alembert duplication, product and difference identities, and the forcing theorem that a monotone solution of the composition law lies in the cosh family.
proof idea
Unfold MonotoneOn on Ici 0: take $0 \le a \le b$ and aim for $\cosh(l a) \le \cosh(l b)$. Apply Real.cosh_le_cosh, which reduces the goal to $|l a| \le |l b|$. Because $l \ge 0$ and $a,b \ge 0$, both products are nonnegative, so abs_of_nonneg removes the absolute values. The remaining inequality is mul_le_mul_of_nonneg_left applied to $a \le b$ with nonnegative factor $l$. No Recognition-specific lemmas are needed; the argument is pure real analysis.
why it matters
Immediate parent is H_jcost_monotoneOn in the same module: after rewriting H(Jcost) as $t \mapsto \cosh(1\cdot t)$, it invokes this theorem at $l=1$. That parent is the non-vacuity witness that $J$ satisfies the order hypothesis; without it the monotone d'Alembert chain would quantify over an empty class.
The chain feeds composition_law_monotone_forces_cosh_family and the broader forcing path to T5 (J-uniqueness via the RCL $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$). Establishing that the actual Recognition cost sits inside the monotone class is what lets the order route pin $J$ rather than an abstract solution set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.