IndisputableMonolith.Verification.JlogNonnegCert

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Jlog Non-Negativity Certificate
   6
   7This audit certificate packages the **non-negativity** property of the log-domain cost:
   8
   9\[
  10  \forall t \in \mathbb{R}, \quad J_{\log}(t) \geq 0
  11\]
  12
  13## Why this matters for the certificate chain
  14
  15Combined with `JlogZeroCert` (Jlog(t) = 0 ⟺ t = 0), this theorem proves that:
  16
  171. **Jlog ≥ 0 everywhere**: The log-domain cost is never negative
  182. **Jlog(0) = 0 is the global minimum**: Since Jlog ≥ 0 and Jlog(0) = 0
  19
  20This establishes that t = 0 (equivalently x = 1 in the original domain) is the
  21unique global minimizer of the cost function, with minimum value 0.
  22
  23## Proof approach
  24
  25From Jlog(t) = Jcost(exp(t)) = (exp(t) - 1)² / (2·exp(t)):
  26- Numerator (exp(t) - 1)² ≥ 0 (always non-negative)
  27- Denominator 2·exp(t) > 0 (always positive)
  28- Therefore Jlog(t) ≥ 0
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Verification
  33namespace JlogNonneg
  34
  35open IndisputableMonolith.Cost
  36
  37structure JlogNonnegCert where
  38  deriving Repr
  39
  40/-- Verification predicate: Jlog(t) ≥ 0 for all t.
  41
  42This certifies the non-negativity of the log-domain cost function. -/
  43@[simp] def JlogNonnegCert.verified (_c : JlogNonnegCert) : Prop :=
  44  ∀ t : ℝ, 0 ≤ Jlog t
  45
  46@[simp] theorem JlogNonnegCert.verified_any (c : JlogNonnegCert) :
  47    JlogNonnegCert.verified c := by
  48  intro t
  49  exact Jlog_nonneg t
  50
  51end JlogNonneg
  52end Verification
  53end IndisputableMonolith
  54