Pith. sign in
module module high

IndisputableMonolith.Cost.Convexity

show as:
view Lean formalization →

The Cost.Convexity module proves that cosh is strictly convex on the reals and transfers the property to Jcost on positive reals via the identity J(x) = cosh(log x) - 1. Researchers citing T5 uniqueness or variational principles in the action modules would reference these lemmas. Proofs proceed by the second-derivative test on cosh followed by algebraic transfer and chain-rule derivative calculations.

claimThe map \( x \mapsto \cosh x \) is strictly convex on \( \mathbb{R} \). The map \( x \mapsto J(x) = \cosh(\log x) - 1 \) is strictly convex on \( (0,\infty) \).

background

The module sits inside the Cost domain and imports the definition of Jcost together with its logarithmic form from the upstream Cost module. It also pulls standard convexity and derivative machinery from Mathlib. The local setting is the one-dimensional cost space on which the recognition composition law forces J to satisfy J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).

proof idea

The central lemma establishes cosh_strictly_convex by noting that the second derivative equals cosh itself and is everywhere positive. Jlog_eq_cosh_sub_one then transfers the property to Jlog_strictConvexOn. Remaining lemmas compute first and second derivatives of Jcost by the chain rule and record positivity of the first derivative for x > 1.

why it matters in Recognition Science

The convexity statements supply the strict-convexity hypothesis required by CostUniqueness for the T5 uniqueness theorem. They are imported by Action.FunctionalConvexity to discharge the conditional minimizer witness, by EulerLagrange to obtain the unique stationary path, and by Determinism to guarantee unique ledger updates.

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)