pith. sign in
module module high

IndisputableMonolith.Cost.Convexity

show as:
view Lean formalization →

The Cost.Convexity module proves strict convexity of the J-cost function on positive reals by relating it to cosh via a logarithmic substitution. Researchers on variational principles and uniqueness theorems cite these lemmas to guarantee unique minimizers. Proofs apply the second-derivative test to cosh and transfer convexity through the change of variables.

claimThe map $J(x) = (x + x^{-1})/2 - 1$ is strictly convex on $(0,∞)$. Equivalently, $J(x) = cosh(log x) - 1$ and $cosh$ is strictly convex on $ℝ$ because its second derivative equals itself and remains positive.

background

Recognition Science introduces the J-cost via the Recognition Composition Law, yielding the explicit form $J(x) = (x + x^{-1})/2 - 1$, which is identical to $cosh(log x) - 1$. The module supplies the analytic convexity infrastructure required by action functionals and determinism arguments. It imports Mathlib convexity and derivative machinery while building directly on the base Cost module that defines Jcost and the composition law.

proof idea

The module first shows cosh is strictly convex on $ℝ$ by verifying that its second derivative equals cosh and is everywhere positive. It next records the identity $Jlog(x) = cosh(log x) - 1$. Strict convexity of Jlog on $(0,∞)$ then follows by composition of the strictly convex cosh with the strictly increasing logarithm, using standard calculus transfer lemmas from Mathlib.

why it matters in Recognition Science

These results are imported by CostUniqueness to complete the main T5 uniqueness theorem for any cost functional obeying symmetry, normalization, strict convexity and calibration. They also feed the Euler-Lagrange derivations in Action.EulerLagrange and the determinism claim that strict convexity forces unique minimizers. The module thereby closes the analytic step between the functional equation and the variational principle.

scope and limits

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)