washburn_uniqueness_of_contDiff

formal source

 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
 201  have h_H0 : Hf 0 = 1 := by
 202    dsimp [Hf]
 203    simpa [H, G, IsNormalized] using hNorm
 204  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 205    intro t u
 206    have hG := h_direct t u
 207    have h_goal :
 208        (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
 209      calc
 210        (Gf (t + u) + 1) + (Gf (t - u) + 1)
 211            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
 212        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
 213        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
 214    simpa [Hf, H, Gf] using h_goal
 215  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
 216    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
 217      simpa [Gf, G, IsCalibrated] using hCalib
 218    have hderiv : deriv Hf = deriv Gf := by
 219      funext t