IndisputableMonolith.Cost.Calibration

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Calibration: Second Derivative at Unity
   6
   7This module proves that the second derivative of Jlog at zero equals 1,
   8establishing the unit normalization axiom (A4).
   9
  10This calibration fixes the scale uniquely and completes the characterization of J.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Cost
  15
  16open Real
  17
  18/-- Jlog equals cosh t - 1 -/
  19lemma Jlog_eq_cosh (t : ℝ) : Jlog t = Real.cosh t - 1 := Jlog_as_cosh t
  20
  21/-- Jlog has derivative sinh -/
  22lemma hasDerivAt_Jlog_new (t : ℝ) : HasDerivAt Jlog (sinh t) t := by
  23  have heq : Jlog = fun s => cosh s - 1 := by
  24    funext s
  25    exact Jlog_eq_cosh s
  26  rw [heq]
  27  exact (hasDerivAt_cosh t).sub_const 1
  28
  29/-- First derivative of Jlog is sinh -/
  30lemma deriv_Jlog (t : ℝ) : deriv Jlog t = sinh t := by
  31  exact (hasDerivAt_Jlog_new t).deriv
  32
  33/-- Second derivative of Jlog is cosh -/
  34lemma deriv2_Jlog (t : ℝ) : deriv (deriv Jlog) t = cosh t := by
  35  have h1 : deriv Jlog = sinh := by
  36    funext s; exact deriv_Jlog s
  37  rw [h1]
  38  exact (hasDerivAt_sinh t).deriv
  39
  40/-- The calibration theorem: second derivative at zero equals 1 -/
  41theorem Jlog_second_deriv_at_zero : deriv (deriv Jlog) 0 = 1 := by
  42  rw [deriv2_Jlog]
  43  exact cosh_zero
  44
  45/-- Alternative formulation: Jlog has unit curvature at the identity -/
  46theorem Jlog_unit_curvature : deriv (deriv Jlog) 0 = 1 :=
  47  Jlog_second_deriv_at_zero
  48
  49/-- Identity: (Jcost ∘ exp) equals Jlog pointwise. -/
  50lemma Jcost_comp_exp_eq_Jlog : (fun t : ℝ => Jcost (Real.exp t)) = Jlog := rfl
  51
  52/-- Calibration for Jcost in log-coordinates: second derivative at zero is 1. -/
  53theorem Jcost_comp_exp_second_deriv_at_zero :
  54    deriv (deriv (fun t : ℝ => Jcost (Real.exp t))) 0 = 1 := by
  55  -- Jcost ∘ exp = Jlog by definition
  56  have h : (fun t : ℝ => Jcost (Real.exp t)) = Jlog := rfl
  57  rw [h]
  58  exact Jlog_second_deriv_at_zero
  59
  60/-- Package the calibration axiom -/
  61class UnitCurvature (F : ℝ → ℝ) : Prop where
  62  second_deriv_at_identity : deriv (deriv (F ∘ exp)) 0 = 1
  63
  64instance : UnitCurvature Jcost where
  65  second_deriv_at_identity := Jcost_comp_exp_second_deriv_at_zero
  66
  67end Cost
  68end IndisputableMonolith
  69