IndisputableMonolith.Verification.JlogStrictConvexCert

   1import Mathlib
   2import IndisputableMonolith.Cost.Convexity
   3
   4/-!
   5# Jlog Strict Convexity Certificate
   6
   7This audit certificate packages the **strict convexity** of the log-domain cost:
   8
   9\[
  10  J_{\log} : \mathbb{R} \to \mathbb{R} \text{ is strictly convex on } \mathbb{R}
  11\]
  12
  13## Why this matters for the certificate chain
  14
  15Strict convexity is a powerful property that implies:
  16
  171. **Unique global minimum**: Any critical point is the unique global minimizer
  182. **Gradient characterization**: ∇Jlog(t) = 0 ⟺ t is the unique minimizer
  193. **Strong duality**: For optimization problems involving Jlog
  20
  21Combined with JlogZeroCert (Jlog(0) = 0) and JlogNonnegCert (Jlog ≥ 0),
  22strict convexity provides an independent route to uniqueness of the cost minimum.
  23
  24## Proof approach
  25
  26Since Jlog(t) = cosh(t) - 1:
  271. cosh is strictly convex on ℝ (second derivative cosh'' = cosh > 0)
  282. Subtracting a constant preserves strict convexity
  293. Therefore Jlog = cosh - 1 is strictly convex on ℝ
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Verification
  34namespace JlogStrictConvex
  35
  36open IndisputableMonolith.Cost
  37open Set
  38
  39structure JlogStrictConvexCert where
  40  deriving Repr
  41
  42/-- Verification predicate: Jlog is strictly convex on ℝ.
  43
  44This certifies the strict convexity of the log-domain cost function. -/
  45@[simp] def JlogStrictConvexCert.verified (_c : JlogStrictConvexCert) : Prop :=
  46  StrictConvexOn ℝ univ Jlog
  47
  48@[simp] theorem JlogStrictConvexCert.verified_any (c : JlogStrictConvexCert) :
  49    JlogStrictConvexCert.verified c := by
  50  exact Jlog_strictConvexOn
  51
  52end JlogStrictConvex
  53end Verification
  54end IndisputableMonolith
  55