IndisputableMonolith.Verification.JcostCoshFormCert

   1import Mathlib
   2import IndisputableMonolith.Cost.FunctionalEquation
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace JcostCoshForm
   7
   8open IndisputableMonolith.Cost.FunctionalEquation
   9open Real
  10
  11/-!
  12# J-Cost Cosh Form Certificate
  13
  14This certificate packages the proof that the J-cost function, when expressed in
  15log-coordinates via G(t) = J(exp(t)), equals cosh(t) - 1.
  16
  17## Key Results
  18
  191. **Cosh representation**: G_J(t) = J(exp(t)) = cosh(t) - 1 for all t ∈ ℝ
  20
  212. **Cosh-type functional identity**: G_J satisfies the d'Alembert-like identity
  22   G(t+u) + G(t-u) = 2·G(t)·G(u) + 2·(G(t) + G(u))
  23
  24## Why this matters for the certificate chain
  25
  26These identities are foundational for T5 cost uniqueness:
  27- The cosh representation connects J to hyperbolic geometry
  28- The functional identity shows J's structure is determined by algebraic constraints
  29- Combined with ODE uniqueness (H'' = H → H = cosh) and d'Alembert symmetry,
  30  this establishes that J is the unique cost satisfying these constraints
  31
  32## Mathematical Content
  33
  34The J-cost is defined as J(x) = (x + x⁻¹)/2 - 1 for x > 0.
  35
  36In log-coordinates: G_J(t) = J(exp(t)) = (exp(t) + exp(-t))/2 - 1 = cosh(t) - 1.
  37
  38The cosh-add identity for G_J:
  39  G_J(t+u) + G_J(t-u) = 2·G_J(t)·G_J(u) + 2·(G_J(t) + G_J(u))
  40
  41This is distinct from the d'Alembert equation H(t+u) + H(t-u) = 2·H(t)·H(u)
  42but is related to it (the extra linear terms arise from the "-1" shift).
  43-/
  44
  45structure JcostCoshFormCert where
  46  deriving Repr
  47
  48/-- Verification predicate: J-cost has the cosh form in log-coordinates. -/
  49@[simp] def JcostCoshFormCert.verified (_c : JcostCoshFormCert) : Prop :=
  50  -- 1) G_J(t) = cosh(t) - 1 for all t
  51  (∀ t : ℝ, G Cost.Jcost t = Real.cosh t - 1)
  52  ∧
  53  -- 2) G_J satisfies the cosh-add functional identity
  54  CoshAddIdentity Cost.Jcost
  55
  56/-- Top-level theorem: the certificate verifies. -/
  57@[simp] theorem JcostCoshFormCert.verified_any (c : JcostCoshFormCert) :
  58    JcostCoshFormCert.verified c := by
  59  constructor
  60  · -- G_J(t) = cosh(t) - 1
  61    exact Jcost_G_eq_cosh_sub_one
  62  · -- CoshAddIdentity Jcost
  63    exact Jcost_cosh_add_identity
  64
  65end JcostCoshForm
  66end Verification
  67end IndisputableMonolith
  68