IndisputableMonolith.Verification.JcostCoshIdentityCert

   1import Mathlib
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4/-!
   5# J-cost Cosh Functional Identity Certificate
   6
   7This audit certificate packages the **cosh-type functional identity** for the RS cost kernel.
   8
   9In log-coordinates (where G(t) = J(exp(t))), the identity states:
  10
  11\[
  12  G(t+u) + G(t-u) = 2 \cdot G(t) \cdot G(u) + 2 \cdot (G(t) + G(u))
  13\]
  14
  15## Why this matters for the certificate chain
  16
  17The cosh functional equation is the characteristic identity that:
  18
  191. **Characterizes cosh**: Solutions to this functional equation with appropriate
  20   regularity conditions are exactly scalar multiples of cosh (shifted)
  212. **Underpins T5 (uniqueness)**: The cost uniqueness theorem uses this identity
  22   to show J is the unique symmetric, normalized, strictly convex cost
  233. **Connects to d'Alembert**: This is a variant of the d'Alembert functional equation
  24   f(x+y) + f(x-y) = 2f(x)f(y), which characterizes cosh and cos
  25
  26## Proof approach
  27
  28Direct calculation using:
  29- exp(t+u) = exp(t)·exp(u)
  30- exp(t-u) = exp(t)/exp(u)
  31- J(x) = (x + x⁻¹)/2 - 1
  32
  33The identity follows from algebraic manipulation.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Verification
  38namespace JcostCoshIdentity
  39
  40open IndisputableMonolith.Cost.FunctionalEquation
  41
  42structure JcostCoshIdentityCert where
  43  deriving Repr
  44
  45/-- Verification predicate: J satisfies the cosh-type functional identity in log-coordinates.
  46
  47For G(t) = J(exp(t)), we have:
  48G(t+u) + G(t-u) = 2·G(t)·G(u) + 2·(G(t) + G(u))
  49
  50This characterizes J as having the same functional structure as cosh - 1. -/
  51@[simp] def JcostCoshIdentityCert.verified (_c : JcostCoshIdentityCert) : Prop :=
  52  CoshAddIdentity IndisputableMonolith.Cost.Jcost
  53
  54@[simp] theorem JcostCoshIdentityCert.verified_any (c : JcostCoshIdentityCert) :
  55    JcostCoshIdentityCert.verified c := by
  56  exact Jcost_cosh_add_identity
  57
  58end JcostCoshIdentity
  59end Verification
  60end IndisputableMonolith
  61