pith. sign in
theorem

Jcost_strictConvexOn_pos

proved
show as:
module
IndisputableMonolith.Cost.Convexity
domain
Cost
line
123 · github
papers citing
2 papers (below)

plain-language theorem explainer

The cost function J(x) = (x + x^{-1})/2 - 1 is strictly convex on the positive reals. Researchers proving uniqueness of the cost function under the Recognition Composition Law cite this regularity property. The argument applies the second-derivative criterion for strict convexity on an open interval after confirming continuity and computing the second derivative explicitly.

Claim. The map $xmapsto frac12(x + x^{-1}) - 1$ is strictly convex on the open interval $(0,infty)$.

background

The module establishes convexity of Jlog(t) = cosh(t) - 1 on the reals and of the cost function J on the positives; these properties support the uniqueness theorem T5. The cost function satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Upstream lemmas establish that the first derivative equals (1 - x^{-2})/2 and the second equals x^{-3}.

proof idea

The proof invokes strictConvexOn_of_deriv2_pos on the convex set (0, ∞). Continuity of J follows by unfolding its definition and applying continuity of addition, division by constants, and inversion on positives. For the interior condition it shows the second derivative equals JcostDeriv' x, which reduces to x^{-3} and is positive by zpow_pos.

why it matters

This supplies the strict convexity hypothesis required by Jcost_regularity_cert and by unique_cost_on_pos_from_rcl, the main unconditional T5 statement on positive reals. It also enters the unique_minimizer_principle for deterministic dynamics and the information cost axioms. The result closes the regularity step in the J-uniqueness forcing chain T5, consistent with the Recognition Composition Law and the eight-tick octave.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 2 of 2)