IndisputableMonolith.Verification.JlogDerivCert

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Jlog Derivative Certificate
   6
   7This audit certificate packages the **derivative formula** for the log-domain cost:
   8
   9\[
  10  \frac{d}{dt} J_{\log}(t) = \sinh(t)
  11\]
  12
  13## Why this matters for the certificate chain
  14
  15The derivative formula connects Jlog to the hyperbolic sine:
  16
  171. **Critical point**: At t = 0, sinh(0) = 0, so Jlog'(0) = 0 (stationary point)
  182. **Sign analysis**: sinh(t) < 0 for t < 0, sinh(t) > 0 for t > 0
  19   - This proves t = 0 is a local minimum
  203. **Monotonicity**: Jlog is decreasing on (-∞, 0) and increasing on (0, ∞)
  21
  22Combined with strict convexity, this provides the calculus-based proof that
  23t = 0 is the unique global minimum.
  24
  25## Proof approach
  26
  27Since Jlog(t) = cosh(t) - 1:
  28- d/dt cosh(t) = sinh(t)
  29- d/dt (-1) = 0
  30- Therefore d/dt Jlog(t) = sinh(t)
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Verification
  35namespace JlogDeriv
  36
  37open IndisputableMonolith.Cost
  38
  39structure JlogDerivCert where
  40  deriving Repr
  41
  42/-- Verification predicate: The derivative of Jlog at t is sinh(t).
  43
  44This certifies the derivative formula for the log-domain cost function. -/
  45@[simp] def JlogDerivCert.verified (_c : JlogDerivCert) : Prop :=
  46  ∀ t : ℝ, HasDerivAt Jlog (Real.sinh t) t
  47
  48@[simp] theorem JlogDerivCert.verified_any (c : JlogDerivCert) :
  49    JlogDerivCert.verified c := by
  50  intro t
  51  exact hasDerivAt_Jlog t
  52
  53end JlogDeriv
  54end Verification
  55end IndisputableMonolith
  56