dAlembert_cosh_solution_of_contDiff

formal source

 167  linarith
 168
 169/-- `C²` d'Alembert solutions are determined by calibration and equal `cosh`. -/
 170theorem dAlembert_cosh_solution_of_contDiff
 171    (Hf : ℝ → ℝ)
 172    (h_one : Hf 0 = 1)
 173    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
 174    (h_diff : ContDiff ℝ 2 Hf)
 175    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
 176    ∀ t, Hf t = Real.cosh t := by
 177  have h_ode : ∀ t, deriv (deriv Hf) t = Hf t :=
 178    dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
 179  have h_even : Function.Even Hf := dAlembert_even Hf h_one h_dAlembert
 180  have h_diff0 : DifferentiableAt ℝ Hf 0 :=
 181    (contDiffTwo_differentiable h_diff).differentiableAt
 182  have h_deriv_zero : deriv Hf 0 = 0 :=
 183    even_deriv_at_zero Hf h_even h_diff0
 184  exact ode_cosh_uniqueness_contdiff Hf h_diff h_ode h_one h_deriv_zero
 185
 186/-- Sharpened T5 surface:
 187normalization, the composition law, calibration, and `C²` regularity of `H = G + 1`
 188already force the canonical reciprocal cost. Reciprocal symmetry is derived, not assumed. -/
 189theorem washburn_uniqueness_of_contDiff
 190    (F : ℝ → ℝ)
 191    (hNorm : IsNormalized F)
 192    (hComp : SatisfiesCompositionLaw F)
 193    (hCalib : IsCalibrated F)
 194    (h_diff : ContDiff ℝ 2 (H F)) :
 195    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 196  intro x hx
 197  let Gf : ℝ → ℝ := G F
 198  let Hf : ℝ → ℝ := H F
 199  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
 200  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd