IndisputableMonolith.Verification.CoshStrictConvexCert

   1import Mathlib
   2import IndisputableMonolith.Cost.Convexity
   3
   4/-!
   5# Cosh Strict Convexity Certificate
   6
   7This audit certificate packages the **strict convexity** of the hyperbolic cosine:
   8
   9\[
  10  \cosh : \mathbb{R} \to \mathbb{R} \text{ is strictly convex on } \mathbb{R}
  11\]
  12
  13## Why this matters for the certificate chain
  14
  15The hyperbolic cosine is the foundational function underlying the J-cost structure:
  16
  171. **Jlog = cosh - 1**: The log-domain cost is cosh shifted down by 1
  182. **cosh'' = cosh > 0**: The second derivative is always positive
  193. **Strict convexity of Jlog**: Follows directly from cosh's strict convexity
  20
  21This provides the analytical foundation for the uniqueness of the cost minimum:
  22since cosh is strictly convex and Jlog = cosh - 1, the cost function inherits
  23strict convexity, guaranteeing a unique global minimum.
  24
  25## Proof approach
  26
  27A function with positive second derivative on a convex set is strictly convex.
  28For cosh:
  29- First derivative: cosh' = sinh
  30- Second derivative: cosh'' = cosh > 0 everywhere
  31- Therefore cosh is strictly convex on ℝ
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Verification
  36namespace CoshStrictConvex
  37
  38open Set
  39
  40structure CoshStrictConvexCert where
  41  deriving Repr
  42
  43/-- Verification predicate: cosh is strictly convex on ℝ.
  44
  45This certifies the strict convexity of the hyperbolic cosine function. -/
  46@[simp] def CoshStrictConvexCert.verified (_c : CoshStrictConvexCert) : Prop :=
  47  StrictConvexOn ℝ univ Real.cosh
  48
  49@[simp] theorem CoshStrictConvexCert.verified_any (c : CoshStrictConvexCert) :
  50    CoshStrictConvexCert.verified c := by
  51  exact IndisputableMonolith.Cost.cosh_strictly_convex
  52
  53end CoshStrictConvex
  54end Verification
  55end IndisputableMonolith
  56