IndisputableMonolith.Verification.JlogCoshCert

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Jlog = cosh - 1 Certificate
   6
   7This audit certificate packages the **cosh representation** of the log-domain cost:
   8
   9\[
  10  J_{\log}(t) = \cosh(t) - 1
  11\]
  12
  13where Jlog(t) := J(exp(t)).
  14
  15## Why this matters for the certificate chain
  16
  17The identity Jlog = cosh - 1 is fundamental because:
  18
  191. **Connects to hyperbolic geometry**: cosh is the hyperbolic cosine, linking
  20   the cost kernel to non-Euclidean geometry
  212. **Enables ODE characterization**: cosh is the unique solution to y'' = y
  22   with y(0) = 1, y'(0) = 0, so Jlog satisfies y'' = y + 1
  233. **Explains symmetry**: cosh is even, hence Jlog is even (J(x) = J(1/x))
  244. **Underpins convexity**: cosh'' = cosh > 0, so Jlog is strictly convex
  25
  26This identity transforms the multiplicative domain (x > 0) into the additive
  27domain (t ∈ ℝ) where analysis is cleaner.
  28
  29## Proof approach
  30
  31By definition, Jlog(t) = J(exp(t)) = (exp(t) + exp(-t))/2 - 1 = cosh(t) - 1.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Verification
  36namespace JlogCosh
  37
  38open IndisputableMonolith.Cost
  39
  40structure JlogCoshCert where
  41  deriving Repr
  42
  43/-- Verification predicate: Jlog equals cosh - 1.
  44
  45This certifies the fundamental representation of the cost kernel in log-coordinates
  46as a shifted hyperbolic cosine. -/
  47@[simp] def JlogCoshCert.verified (_c : JlogCoshCert) : Prop :=
  48  ∀ t : ℝ, Jlog t = Real.cosh t - 1
  49
  50@[simp] theorem JlogCoshCert.verified_any (c : JlogCoshCert) :
  51    JlogCoshCert.verified c := by
  52  intro t
  53  exact Jlog_as_cosh t
  54
  55end JlogCosh
  56end Verification
  57end IndisputableMonolith
  58