IndisputableMonolith.Foundation.JCostCoshIdentity

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# J-Cost = Cosh - 1 Identity — Beltracchi Response §5
   6
   7J(eʸ) = (eʸ + e⁻ʸ)/2 - 1.
   8
   9This is the non-linear cosh form of J-cost that appears in the
  10strong-field Regge action. Key properties:
  111. J(eʸ) = 0 iff y = 0 (fixed point)
  122. J(eʸ) = J(e⁻ʸ) (symmetry)
  133. J(eʸ) > 0 for y ≠ 0 (strict positivity)
  144. J(eʸ) ≥ 0 always (non-negative)
  15
  16Lean status: 0 sorry, 0 axiom.
  17-/
  18
  19namespace IndisputableMonolith.Foundation.JCostCoshIdentity
  20open Cost
  21
  22/-- J(eʸ) = (eʸ + e⁻ʸ)/2 - 1. -/
  23theorem jcost_exp_cosh_form (y : ℝ) :
  24    Jcost (Real.exp y) = (Real.exp y + Real.exp (-y)) / 2 - 1 := by
  25  rw [Jcost_eq_sq (Real.exp_ne_zero y)]
  26  rw [Real.exp_neg]
  27  field_simp [Real.exp_ne_zero y]
  28  ring
  29
  30/-- J(e⁰) = 0. -/
  31theorem jcost_exp_zero : Jcost (Real.exp 0) = 0 := by
  32  rw [jcost_exp_cosh_form]; simp
  33
  34/-- J(eʸ) = J(e⁻ʸ). -/
  35theorem jcost_exp_symm (y : ℝ) :
  36    Jcost (Real.exp y) = Jcost (Real.exp (-y)) := by
  37  rw [jcost_exp_cosh_form, jcost_exp_cosh_form]
  38  rw [neg_neg]; ring
  39
  40/-- J(eʸ) ≥ 0. -/
  41theorem jcost_exp_nonneg (y : ℝ) : 0 ≤ Jcost (Real.exp y) := by
  42  rw [jcost_exp_cosh_form]
  43  have := Real.add_one_le_exp y
  44  have := Real.add_one_le_exp (-y)
  45  nlinarith [Real.exp_pos y, Real.exp_pos (-y)]
  46
  47/-- J(eʸ) > 0 for y ≠ 0. -/
  48theorem jcost_exp_pos {y : ℝ} (hy : y ≠ 0) : 0 < Jcost (Real.exp y) := by
  49  have hexp_ne_one : Real.exp y ≠ 1 := by
  50    intro h; exact hy (by rwa [Real.exp_eq_one_iff] at h)
  51  exact Jcost_pos_of_ne_one _ (Real.exp_pos y) hexp_ne_one
  52
  53structure JCostCoshCert where
  54  cosh_form : ∀ y : ℝ, Jcost (Real.exp y) = (Real.exp y + Real.exp (-y)) / 2 - 1
  55  zero_at_zero : Jcost (Real.exp 0) = 0
  56  symmetric : ∀ y : ℝ, Jcost (Real.exp y) = Jcost (Real.exp (-y))
  57  nonneg : ∀ y : ℝ, 0 ≤ Jcost (Real.exp y)
  58  pos_off_zero : ∀ {y : ℝ}, y ≠ 0 → 0 < Jcost (Real.exp y)
  59
  60noncomputable def jCostCoshCert : JCostCoshCert where
  61  cosh_form := jcost_exp_cosh_form
  62  zero_at_zero := jcost_exp_zero
  63  symmetric := jcost_exp_symm
  64  nonneg := jcost_exp_nonneg
  65  pos_off_zero := jcost_exp_pos
  66
  67end IndisputableMonolith.Foundation.JCostCoshIdentity
  68