IndisputableMonolith.Foundation.GeneralizedDAlembert.SecondDerivative

   1import IndisputableMonolith.Foundation.GeneralizedDAlembert
   2
   3/-!
   4  Second-derivative obstruction for the continuous-combiner route.
   5
   6  The residual input `continuous_combiner_second_derivative_identity` cannot
   7  be proved from the current hypotheses alone. The quartic log-cost
   8  `G(t) = t^4`, already used in the paper as the finite-polynomial-closure
   9  counterexample, has `G''(0) = 0` but `G''(1) = 12`. Hence no function
  10  `ψ` can satisfy
  11
  12    `2 * G''(t) = ψ (G t) * G''(0)`
  13
  14  for every `t`.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace GeneralizedDAlembert
  20namespace SecondDerivative
  21
  22private theorem quartic_second_derivative :
  23    deriv (deriv (fun t : ℝ => t^4)) = fun t => 12*t^2 := by
  24  funext t
  25  rw [show deriv (fun t : ℝ => t^4) = fun t => 4*t^3 by
  26    funext x
  27    norm_num [deriv_pow]]
  28  rw [show deriv (fun t : ℝ => 4*t^3) t = 4 * (3*t^2) by
  29    norm_num [deriv_const_mul, deriv_pow]]
  30  ring
  31
  32theorem quartic_not_aczel_second_derivative_identity :
  33    ¬ AczelSecondDerivativeIdentity (fun t : ℝ => t^4) := by
  34  intro h
  35  rcases h with ⟨ψ, hψ⟩
  36  have h1 := hψ 1
  37  rw [quartic_second_derivative] at h1
  38  norm_num at h1
  39
  40end SecondDerivative
  41end GeneralizedDAlembert
  42end Foundation
  43end IndisputableMonolith
  44