Geometry Cayley Menger Derivatives Has Deriv At Shifted Cubic

A small lemma about cubic polynomials

A cubic polynomial is an expression of the form A + B(x - x₀) + C(x - x₀)² + D(x - x₀)³, where A, B, C, D, and x₀ are real numbers. The declaration hasDerivAt_shifted_cubic establishes a basic fact from single-variable calculus: at the point x = x₀, the derivative of this polynomial equals B. This is exactly what one expects from the power rule, since the constant term A vanishes, the linear term contributes B, and the quadratic and cubic terms contribute zero at x = x₀.

The theorem is proved in the machine-checked library of formal theorems, where every step is verified by the computer. It is stated in a general form, so it applies to any cubic polynomial written in this shifted form. The proof itself is a direct application of the standard rules for derivatives, and it does not rely on any special properties of the coefficients A, B, C, or D.

This lemma is not an end in itself but a tool. In the module that computes partial derivatives of the Cayley-Menger polynomial, this fact is used to read off the gradient from a Taylor expansion. When a function is written as a sum of terms in powers of (x - x₀), the coefficient of the linear term is the derivative at x₀. This lemma makes that identification rigorous for the cubic case.

The declaration does not claim anything about the second or third derivatives, nor does it assert that the polynomial is the best approximation of some other function. It only states the value of the first derivative at the single point x₀. It also does not claim that the coefficients A, C, and D are zero; they can be any real numbers, and the derivative at x₀ remains B regardless.

/-- Derivative of a shifted cubic polynomial at its base point. -/
private theorem hasDerivAt_shifted_cubic (A B C D x₀ : ℝ) :
    HasDerivAt (fun x : ℝ => A + B * (x - x₀) + C * (x - x₀) ^ 2
      + D * (x - x₀) ^ 3) B x₀ := by
  have hx : HasDerivAt (fun x : ℝ => x - x₀) (1 : ℝ) x₀ := by
    simpa using (hasDerivAt_id x₀).sub_const x₀
  have hconst : HasDerivAt (fun _ : ℝ => A) (0 : ℝ) x₀ := hasDerivAt_const x₀ A
  have hlin : HasDerivAt (fun x : ℝ => B * (x - x₀)) B x₀ := by
    have := hx.const_mul B
    simpa using this
  have hsq_raw := hx.pow 2
  have hsq : HasDerivAt (fun x : ℝ => (x - x₀) ^ 2) (0 : ℝ) x₀ := by
    simpa using hsq_raw
  have hquad : HasDerivAt (fun x : ℝ => C * (x - x₀) ^ 2) (0 : ℝ) x₀ := by
    have := hsq.const_mul C
    simpa using this
  have hcb_raw := hx.pow 3
  have hcb : HasDerivAt (fun x : ℝ => (x - x₀) ^ 3) (0 : ℝ) x₀ := by
    simpa using hcb_raw
  have hcubic : HasDerivAt (fun x : ℝ => D * (x - x₀) ^ 3) (0 : ℝ) x₀ := by
    have := hcb.const_mul D
    simpa using this
  have htotal := ((hconst.add hlin).add hquad).add hcubic
  simpa using htotal

What this page does not claim

This lemma does not claim anything about the second or higher derivatives of the polynomial. It does not assert that the polynomial itself is the derivative of some other function. It does not claim that the coefficients A, C, or D are zero.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/CayleyMengerDerivatives.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: