strictConvexOn_cosh
plain-language theorem explainer
The theorem asserts that the hyperbolic cosine function is strictly convex over all real numbers. Researchers establishing the J-uniqueness step T5 in Recognition Science cite this when proving convexity of the associated cost functions. The proof is a one-line wrapper that invokes the second-derivative positivity lemma for cosh.
Claim. The map $tmapsto cosh(t)$ is strictly convex on the real line.
background
The Cost.Convexity module establishes convexity properties required for the J function in Recognition Science. Jlog is defined by Jlog(t) = cosh(t) - 1, which is the logarithmic form of the J-cost J(x) = (x + x^{-1})/2 - 1. The module proves strict convexity of Jlog on R and of Jcost on R_+, both foundational for the T5 uniqueness theorem in the forcing chain. The upstream lemma cosh_strictly_convex states that cosh is strictly convex on R because its second derivative equals cosh itself, which is positive everywhere.
proof idea
This is a one-line wrapper that applies the theorem cosh_strictly_convex.
why it matters
It supplies the base convexity of cosh needed to obtain strict convexity of Jlog, which feeds directly into the uniqueness result for the J function at T5. The parent theorem Jlog_strictConvexOn applies this result after rewriting Jlog as cosh minus one. The step anchors the self-similar fixed point phi and the eight-tick octave structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.