IndisputableMonolith.Verification.JcostStrictConvexCert

   1import Mathlib
   2import IndisputableMonolith.Cost.Convexity
   3
   4/-!
   5# Jcost Strict Convexity Certificate
   6
   7This audit certificate packages the **strict convexity** of the original cost function:
   8
   9\[
  10  J(x) = \frac{x + x^{-1}}{2} - 1 \text{ is strictly convex on } (0, \infty)
  11\]
  12
  13## Why this matters for the certificate chain
  14
  15This certifies the strict convexity of Jcost in its natural domain (positive reals):
  16
  171. **Unique minimum at x = 1**: Strict convexity implies J has at most one critical point
  182. **Second derivative test**: J''(x) = x⁻³ > 0 for all x > 0
  193. **Complements Jlog**: While Jlog is strictly convex on all of ℝ, Jcost is
  20   strictly convex on (0, ∞) — these are equivalent via log/exp correspondence
  21
  22## Proof approach
  23
  24A function with positive second derivative on a convex set is strictly convex.
  25For Jcost:
  26- First derivative: J'(x) = (1 - x⁻²)/2
  27- Second derivative: J''(x) = x⁻³ > 0 for x > 0
  28- Therefore Jcost is strictly convex on (0, ∞)
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Verification
  33namespace JcostStrictConvex
  34
  35open IndisputableMonolith.Cost
  36open Set
  37
  38structure JcostStrictConvexCert where
  39  deriving Repr
  40
  41/-- Verification predicate: Jcost is strictly convex on (0, ∞).
  42
  43This certifies the strict convexity of the cost function on positive reals. -/
  44@[simp] def JcostStrictConvexCert.verified (_c : JcostStrictConvexCert) : Prop :=
  45  StrictConvexOn ℝ (Ioi (0 : ℝ)) Jcost
  46
  47@[simp] theorem JcostStrictConvexCert.verified_any (c : JcostStrictConvexCert) :
  48    JcostStrictConvexCert.verified c := by
  49  exact Jcost_strictConvexOn_pos
  50
  51end JcostStrictConvex
  52end Verification
  53end IndisputableMonolith
  54