cosh_strictly_convex
plain-language theorem explainer
The hyperbolic cosine is strictly convex on the entire real line. Researchers establishing the J-uniqueness result T5 cite this when showing that Jlog(t) = cosh(t) - 1 inherits strict convexity. The proof applies the second-derivative criterion for strict convexity on a convex domain, confirming that the second derivative of cosh equals cosh itself and remains positive everywhere.
Claim. The function $f(x) = {cosh}(x)$ is strictly convex on the domain $ℝ$.
background
The Cost.Convexity module proves convexity of the J functions that appear in the Recognition Science forcing chain. Jlog(t) is defined as cosh(t) - 1 and is strictly convex on ℝ; Jcost(x) is defined as ½(x + x⁻¹) - 1 and is strictly convex on ℝ₊. These properties are required for the uniqueness theorem T5, which identifies J(x) = (x + x⁻¹)/2 - 1 with cosh(log x) - 1.
proof idea
The term proof invokes strictConvexOn_of_deriv2_pos on the universal convex set. It first supplies the continuousOn fact from Real.continuous_cosh. It then shows the second derivative is positive by iterating the derivative operator: the first derivative of cosh is sinh and the second is cosh, after which Real.cosh_pos supplies the strict inequality at every point.
why it matters
This supplies the analytic fact that lets Jlog inherit strict convexity, directly feeding the J-uniqueness step T5 in the T0-T8 forcing chain. The sibling declaration strictConvexOn_cosh simply re-exports the result. The convexity guarantees a unique minimizer for the cost function, which in turn forces the self-similar fixed point phi and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.