Verification Jlog Strict Convex Cert

The strict convexity certificate

The cost function in logarithmic coordinates, a measure of the price of recognition, is strictly convex: its graph curves upward everywhere, like a bowl with no flat spots. Strict convexity means the function has exactly one global minimum, and any point where its slope is zero is that minimum. The certificate named JlogStrictConvexCert is a machine-checked proof of this property, part of a library of formal theorems that auditors can inspect line by line.

The function in question is Jlog(t) = cosh(t) - 1, where cosh is the hyperbolic cosine. Its second derivative is cosh(t), which is positive for every real t, so the function is strictly convex on the entire real line. Subtracting the constant 1 shifts the graph down but does not change its curvature. The certificate packages this argument: it states the predicate StrictConvexOn ℝ univ Jlog, and its companion theorem verified_any supplies the proof for any instance of the certificate.

Why this matters: strict convexity gives an independent route to uniqueness of the cost minimum, alongside other certificates that establish Jlog(0) = 0 and Jlog ≥ 0. If a critical point exists, it is the unique global minimizer; there is no second valley, no plateau, no ambiguity about where the lowest cost sits. For optimization problems involving this cost, the property also enables strong duality, meaning a primal problem and its dual have the same optimal value under mild conditions.

In Recognition Science, the framework models reality as maintaining a ledger, a discrete record of recognition events, with a forced cost. The strict convexity certificate is a verification artifact: it does not derive new physics, but it confirms a structural fact about the cost function that other results rely on. The practical consequence is that when the framework's optimization problems are solved, the solution is well-defined and unique, not a matter of choosing among equally good alternatives.

structure JlogStrictConvexCert where
  deriving Repr

structure JlogStrictConvexCert where
  deriving Repr

What this page does not claim

This certificate does not derive the cost function's uniqueness; it only proves strict convexity of the log-domain form. Strict convexity alone does not establish that a minimum exists; that requires additional conditions such as coercivity. The certificate does not connect Jlog to the physical constants or particle masses in the framework.

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/Verification/JlogStrictConvexCert.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: