even_function_deriv_zero

formal source

 435    At t = 0: -G'(0) = G'(0), hence 2G'(0) = 0, so G'(0) = 0.
 436
 437    This is a standard calculus result. -/
 438theorem even_function_deriv_zero (G : ℝ → ℝ)
 439    (hEven : ∀ t, G (-t) = G t)
 440    (hDiff : DifferentiableAt ℝ G 0) :
 441    deriv G 0 = 0 := by
 442  -- The functions (fun t => G(-t)) and G are equal everywhere
 443  have hfun_eq : (fun t => G (-t)) = G := funext hEven
 444  -- So their derivatives at 0 must be equal
 445  have hderiv_eq : deriv (fun t => G (-t)) 0 = deriv G 0 := by simp only [hfun_eq]
 446  -- Compute deriv (fun t => G(-t)) 0 using chain rule
 447  have hchain : deriv (fun t => G (-t)) 0 = -(deriv G 0) := by
 448    have hcomp : (fun t => G (-t)) = G ∘ (fun t => -t) := rfl
 449    rw [hcomp]
 450    rw [deriv_comp (0 : ℝ) (by simp only [neg_zero]; exact hDiff) differentiable_neg.differentiableAt]
 451    simp only [neg_zero, deriv_neg', mul_neg_one]
 452  -- Now: hderiv_eq says deriv (G ∘ neg) 0 = deriv G 0
 453  --      hchain says deriv (G ∘ neg) 0 = -(deriv G 0)
 454  rw [hchain] at hderiv_eq
 455  linarith
 456
 457/-- **Axiom (Separable Combiner Forces Flat ODE)**: Under the structural axioms,
 458    if P is separable (hence P = 2u + 2v), then G_of F satisfies G'' = 1.
 459
 460    Proof sketch: From G(t+u) + G(t-u) = 2G(t) + 2G(u), differentiate twice in u at u=0:
 461    2G''(t) = 2G''(0) = 2, hence G''(t) = 1. -/
 462theorem separable_combiner_forces_flat :
 463    ∀ F : ℝ → ℝ, ∀ P : ℝ → ℝ → ℝ,
 464    F 1 = 0 →
 465    (∀ x : ℝ, 0 < x → F x = F x⁻¹) →
 466    ContDiff ℝ 2 F →
 467    deriv (deriv (G_of F)) 0 = 1 →
 468    (∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) →