Cost Convexity

Cost convexity

Cost convexity is the shape property of the recognition cost function J that Recognition Science derives from its five founding conditions. A function is strictly convex when the line segment between any two distinct points on its graph lies strictly above the graph itself. For J this means the cost of a mismatch grows faster than linearly as the mismatch moves away from perfect agreement, so the graph is a single bowl with exactly one lowest point. This property is machine-checked, not assumed, and it is foundational for the uniqueness theorem T5, which forces the exact form of J.

The module establishes strict convexity for the two equivalent forms of J. The first form, Jlog(t) = cosh(t) - 1, is strictly convex on the whole real line. The proof uses the fact that the second derivative of cosh is cosh itself, which is always positive. The second form, Jcost(x) = ½(x + x⁻¹) - 1, is strictly convex on the positive reals, the domain where x represents a ratio of recognition magnitudes. Its second derivative is x⁻³, which is positive for every x > 0. The two forms are linked by the substitution x = e^t, so Jcost(e^t) = Jlog(t).

Strict convexity is what makes the cost function well behaved for minimization. A strictly convex function on a convex domain has at most one point where it reaches its minimum. For Jcost on the positive reals, that unique minimum sits at x = 1, where the cost is zero, meaning perfect agreement. The second derivative at that point equals 1, which sets the local curvature scale. Because the minimum is unique and the graph has no flat regions, the forcing chain that builds the rest of Recognition Science has a stable foundation: the cost function cannot wander into multiple equally good states.

THEOREM Jlog_strictConvexOn · IndisputableMonolith/Cost/Convexity.lean

THEOREM Jcost_strictConvexOn_pos · IndisputableMonolith/Cost/Convexity.lean

THEOREM deriv2_Jcost · IndisputableMonolith/Cost/Convexity.lean

THEOREM deriv2_Jcost_one · IndisputableMonolith/Cost/Convexity.lean

What this page does not claim

This answer does not prove the uniqueness theorem T5 itself. This answer does not claim that convexity alone determines the numerical value of J; the five founding conditions are needed for that. This answer does not claim that Jcost is convex on the whole real line; its domain is the positive reals.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Convexity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: