IndisputableMonolith.Verification.JlogZeroCert

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Jlog Zero Characterization Certificate
   6
   7This audit certificate packages the **unique zero** property of the log-domain cost:
   8
   9\[
  10  J_{\log}(t) = 0 \iff t = 0
  11\]
  12
  13## Why this matters for the certificate chain
  14
  15The Jlog function (Jcost ∘ exp) measures "cost" in log-coordinates. This theorem
  16establishes that:
  17
  181. **Jlog(0) = 0**: The origin is a zero of the log-domain cost
  192. **Jlog(t) = 0 ⟹ t = 0**: This is the *only* zero
  20
  21Combined with Jlog_nonneg (Jlog ≥ 0), this proves that t = 0 is the unique
  22global minimum of Jlog, which translates to x = 1 being the unique minimum
  23of Jcost (since exp(0) = 1).
  24
  25## Proof approach
  26
  27Jlog(t) = Jcost(exp(t)) = (1/2)(exp(t) + exp(-t)) - 1 = cosh(t) - 1
  28
  29Since cosh(t) = 1 ⟺ t = 0 and exp(t) = 1 ⟺ t = 0:
  30- Jlog(t) = 0 ⟺ cosh(t) = 1 ⟺ t = 0
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Verification
  35namespace JlogZero
  36
  37open IndisputableMonolith.Cost
  38
  39structure JlogZeroCert where
  40  deriving Repr
  41
  42/-- Verification predicate: Jlog(t) = 0 ⟺ t = 0.
  43
  44This certifies the unique zero characterization of the log-domain cost. -/
  45@[simp] def JlogZeroCert.verified (_c : JlogZeroCert) : Prop :=
  46  ∀ t : ℝ, Jlog t = 0 ↔ t = 0
  47
  48@[simp] theorem JlogZeroCert.verified_any (c : JlogZeroCert) :
  49    JlogZeroCert.verified c := by
  50  intro t
  51  exact Jlog_eq_zero_iff t
  52
  53end JlogZero
  54end Verification
  55end IndisputableMonolith
  56