Geometry Cayley Menger Derivatives Has Deriv At Cm3 Partial3

A derivative in closed form

The Cayley-Menger polynomial is a formula that takes the six squared edge lengths of a tetrahedron and returns a number related to its volume. For a tetrahedron with vertices 0, 1, 2, and 3, the edge (1,2) is the third in the standard ordering. The declaration hasDerivAt_cm3_partial3 proves that this polynomial has a derivative with respect to that single edge length, and it gives the derivative as an explicit quadratic polynomial in the six squared lengths.

The derivative itself is the rate at which the polynomial changes when you nudge only the (1,2) edge while holding the other five fixed. The theorem states that this rate equals the expression cm3_partial3, a specific formula: twice the quantity a2 times (a0 + a1 + a4 + a5 - a2 - a3) minus a2 times a3, plus a0 times a5 plus a1 times a4, minus a0 times a1 minus a4 times a5. Here a0 through a5 are the six squared edge lengths in the fixed order, so a3 is the squared length of edge (1,2) itself.

The proof works by writing the polynomial as a Taylor expansion around any point. The theorem cm3_update_taylor shows that changing one edge length by a small amount t changes the polynomial by the gradient times t, plus a quadratic term and a cubic term. The cubic coefficient turns out to be zero for a single-coordinate change, which makes the derivative exact and not merely an approximation. The machine-checked library of formal theorems verifies this by direct algebraic manipulation.

This derivative is a building block for a larger project. The framework's library uses these six partial derivatives to construct the Regge second-variation matrix, which measures how the polynomial curves as multiple edges change together. That matrix is later compared with the areas of triangular faces through a chain rule. The derivative itself is a purely formal statement about a polynomial; it does not require the six lengths to correspond to an actual tetrahedron in space.

The theorem does not claim that the polynomial is differentiable everywhere in the sense of a smooth manifold, although that is true. It does not assert that the derivative is nonzero, nor that the polynomial has a minimum or maximum at any point. It only establishes the exact slope along one coordinate direction, and it does so for every choice of six real numbers, whether or not they form a valid tetrahedron.

theorem hasDerivAt_cm3_partial3 (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cm3 (Function.update a 3 t)) (cm3_partial3 a) (a 3) := by
  simpa [cm3_grad] using hasDerivAt_cm3_grad a 3

/-- Partial derivative of `cm3` with respect to `a 3` (= λ = squared edge (1,2)). -/
def cm3_partial3 (a : SqEdges) : ℝ :=
  2 * ( a 2 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3) - a 2 * a 3
      + a 0 * a 5 + a 1 * a 4
      - a 0 * a 1 - a 4 * a 5 )

/-- A specialised corollary of the Taylor identity: when only the
`i`-th coordinate is perturbed, the formula collapses to the 1-D
restriction of `cm3` along that coordinate.  This is what feeds the
six per-edge partial-derivative theorems. -/
theorem cm3_update_taylor (a : SqEdges) (i : Fin 6) (t : ℝ) :
    cm3 (Function.update a i (a i + t)) =
      cm3 a + (cm3_grad a i) * t
      + cm3_quadratic a (singlePerturb i t) + cm3_cubic (singlePerturb i t) := by
  have hpt : (fun j : Fin 6 => a j + (singlePerturb i t) j)
              = Function.update a i (a i + t) := by
    funext j
    by_cases hij : j = i
    · subst hij
      simp [singlePerturb_at]
    · have h1 : (singlePerturb i t) j = 0 := singlePerturb_ne i j hij t
      have h2 : Function.update a i (a i + t) j = a j := by
        simp [Function.update, hij]
      rw [h1, h2]
      ring
  have h := cm3_taylor a (singlePerturb i t)
  rw [hpt] at h
  rw [h]
  have hlin : cm3_linear a (singlePerturb i t) = cm3_grad a i * t := by
    unfold cm3_linear cm3_grad singlePerturb
    fin_cases i <;> simp [cm3_partial0, cm3_partial1, cm3_partial2,
            cm3_partial3, cm3_partial4, cm3_partial5]
  linarith [hlin]

/-- Cubic-in-`t` coefficient of the single-coordinate correction.  In each
case there is no `t³` contribution because the cm3 polynomial is degree 2 in
each *individual* squared-edge coordinate. -/
def cm3_cubic_coeff : Fin 6 → ℝ := fun _ => 0

/-- Hessian diagonal entries with respect to the squared-edge coordinates.
Since `cm3 (a.update i (a i + t))` has quadratic coefficient
`cm3_quadratic_coeff i a`, the second derivative in coordinate `i` is
`2 * cm3_quadratic_coeff i a`. -/
def cm3_hessianDiag (a : SqEdges) (i : Fin 6) : ℝ :=
  2 * cm3_quadratic_coeff i a

What this page does not claim

The theorem does not claim that the six edge lengths form a valid tetrahedron. It does not claim the derivative is nonzero or that the polynomial has a critical point. It does not claim differentiability in the sense of a smooth manifold, although that is separately established.

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: