 203/-- RS-native CPM constants for cone projection. Placeholders are kept
 204symbolic by default for `C_eng` and `C_disp`; domain instantiations can
 205refine them. -/
 206def coneConstants : Constants := {
 207  Knet  := 1,
 208  Cproj := 2,
 209  Ceng  := 1,
 210  Cdisp := 1,
 211  Knet_nonneg := by norm_num,
 212  Cproj_nonneg := by norm_num,
 213  Ceng_nonneg := by norm_num,
 214  Cdisp_nonneg := by norm_num
 215}
 216
 217@[simp] lemma cone_Knet_eq_one : coneConstants.Knet = 1 := rfl
 218@[simp] lemma cone_Cproj_eq_two : coneConstants.Cproj = 2 := rfl
 219@[simp] lemma cone_Ceng_eq_one : coneConstants.Ceng = 1 := rfl
 220@[simp] lemma cone_Cdisp_eq_one : coneConstants.Cdisp = 1 := rfl
 221
 222/-- J-cost log-coordinate normalization used as justification hook:
 223`deriv (deriv (J ∘ exp)) 0 = 1`. -/
 224lemma Jcost_log_second_deriv_normalized :
 225  deriv (deriv (fun t : ℝ => IndisputableMonolith.Cost.Jcost (Real.exp t))) 0 = 1 := by
 226  -- Define f(t) = Jcost (exp t) with no cosh expansion
 227  set f : ℝ → ℝ := fun t => ((Real.exp t + Real.exp (-t)) / 2) - 1 with hfdef
 228  have hf_eq : (fun t : ℝ => IndisputableMonolith.Cost.Jcost (Real.exp t)) = f := by
 229    funext t; simp [hfdef, IndisputableMonolith.Cost.Jcost_exp]
 230  -- First derivative of f: f'(t) = (exp t - exp (-t)) / 2
 231  have h_deriv_f : deriv f = fun t => (Real.exp t - Real.exp (-t)) / 2 := by
 232    funext t
 233    -- derivative of exp and exp∘neg
 234    have h1 : HasDerivAt (fun s => Real.exp s) (Real.exp t) t := Real.hasDerivAt_exp t
 235    have h2 : HasDerivAt (fun s => Real.exp (-s)) (- Real.exp (-t)) t := by
 236      simpa using (Real.hasDerivAt_exp (-t)).comp t (hasDerivAt_neg t)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.