Encyclopedia Geometry Geometry Cofactor Polynomial Has Deriv At Cm Cofactor3 Poly 34 Along Coord

ARTICLE 2 claims 2 theorems

Geometry Cofactor Polynomial Has Deriv At Cm Cofactor3 Poly 34 Along Coord

This theorem gives a named, explicit formula for the rate of change of a specific cofactor of a tetrahedron's Cayley-Menger matrix as one edge length varies.

Verify this page

A derivative for a tetrahedron's cofactor

In geometry, the Cayley-Menger matrix encodes the six edge lengths of a tetrahedron in a way that lets you compute its volume and related quantities. A cofactor of this matrix is a signed determinant of a smaller matrix, formed by deleting one row and one column. This declaration concerns the cofactor in row 3, column 4, viewed as a function of the six squared edge lengths. The theorem states that this cofactor is differentiable with respect to any one of those six lengths, and it gives the derivative explicitly as a named polynomial, cmCofactorPartial.

The statement is precise: for any choice of one of the six edge coordinates, and for any tetrahedron (specified by its squared edge lengths), the function that takes a new value for that edge and returns the cofactor has a derivative at the original edge length. That derivative equals the polynomial cmCofactorPartial evaluated at the original lengths. In symbols, for each edge index k and each edge-length vector a, the derivative of cmCofactor3Poly 3 4 with respect to coordinate k is cmCofactorPartial 3 4 k a.

This is a technical but useful result. It turns a question about a derivative of a complicated determinant into a question about evaluating a specific polynomial. Downstream, this allows dihedral-angle calculus to refer to named polynomial partials instead of opaque derivative terms. The theorem is machine-checked, meaning a computer has verified the proof step by step from the definitions.

The declaration does not claim that the cofactor is differentiable with respect to all six edges simultaneously, nor does it provide a geometric interpretation of the derivative. It also does not state anything about the volume of the tetrahedron itself, only about this particular cofactor. The result is a formal statement about a polynomial function, not a physical law.

THEOREM hasDerivAt_cmCofactor3Poly_34_along_coord · cmCofactorPartial · IndisputableMonolith/Geometry/CofactorPolynomial.lean
hasDerivAt_cmCofactor3Poly_34_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean:985 
/-- Closed-form coordinate derivative of the `(3,4)` cofactor polynomial. -/
theorem hasDerivAt_cmCofactor3Poly_34_along_coord
    (k : Fin 6) (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t))
      (cmCofactorPartial 3 4 k a) (a k) := by
  have hfun :
      (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t)) =
        (fun t : ℝ => cmCofactor3Poly 3 4 a
          + cmCofactorPartial 3 4 k a * (t - a k)
          + (if k = 0 then -1 else 0) * (t - a k) ^ 2
          + 0 * (t - a k) ^ 3) := by
    funext t
    have h := cmCofactor3Poly_34_update_polyform a k (t - a k)
    have hbase : a k + (t - a k) = t := by ring
    rw [hbase] at h
    simpa using h
  rw [hfun]
  exact hasDerivAt_shifted_cubic (cmCofactor3Poly 3 4 a)
    (cmCofactorPartial 3 4 k a) (if k = 0 then -1 else 0) 0 (a k)
cmCofactorPartial · IndisputableMonolith/Geometry/CofactorPolynomial.lean:56 
/-- Explicit partial derivative of a cofactor polynomial with respect to one
squared-edge coordinate. -/
def cmCofactorPartial (r c : Fin 5) (k : Fin 6) (a : SqEdges) : ℝ :=
  match r.val, c.val, k.val with
  | 0, 0, 0 => -2 * (a 2) * (a 3) * (a 5) - 2 * (a 1) * (a 4) * (a 5) + 2 * (a 0) * (a 5) ^ 2
  | 0, 0, 1 => -2 * (a 2) * (a 3) * (a 4) + 2 * (a 1) * (a 4) ^ 2 - 2 * (a 0) * (a 4) * (a 5)
  | 0, 0, 2 => 2 * (a 2) * (a 3) ^ 2 - 2 * (a 1) * (a 3) * (a 4) - 2 * (a 0) * (a 3) * (a 5)
  | 0, 0, 3 => 2 * (a 2) ^ 2 * (a 3) - 2 * (a 1) * (a 2) * (a 4) - 2 * (a 0) * (a 2) * (a 5)
  | 0, 0, 4 => -2 * (a 1) * (a 2) * (a 3) + 2 * (a 1) ^ 2 * (a 4) - 2 * (a 0) * (a 1) * (a 5)
  | 0, 0, 5 => -2 * (a 0) * (a 2) * (a 3) - 2 * (a 0) * (a 1) * (a 4) + 2 * (a 0) ^ 2 * (a 5)
  | 0, 1, 0 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5)
  | 0, 1, 1 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4)
  | 0, 1, 2 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2
  | 0, 1, 3 => -2 * (a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5)
  | 0, 1, 4 => -2 * (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
  | 0, 1, 5 => -2 * (a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3)
  | 0, 2, 0 => -(a 5) ^ 2 + (a 2) * (a 5) + (a 1) * (a 5)
  | 0, 2, 1 => (a 4) * (a 5) - 2 * (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5)
  | 0, 2, 2 => (a 3) * (a 5) - 2 * (a 2) * (a 3) - 2 * (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
  | 0, 2, 3 => (a 2) * (a 5) - (a 2) ^ 2 + (a 1) * (a 2)
  | 0, 2, 4 => (a 1) * (a 5) + (a 1) * (a 2) - (a 1) ^ 2
  | 0, 2, 5 => (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 2) + (a 0) * (a 1)
  | 0, 3, 0 => (a 4) * (a 5) + (a 2) * (a 5) - 2 * (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5)
  | 0, 3, 1 => -(a 4) ^ 2 + (a 2) * (a 4) + (a 0) * (a 4)
  | 0, 3, 2 => (a 3) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5) - 2 * (a 0) * (a 4) + (a 0) * (a 3)
  | 0, 3, 3 => (a 2) * (a 4) - (a 2) ^ 2 + (a 0) * (a 2)
  | 0, 3, 4 => (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) - 2 * (a 0) * (a 2) + (a 0) * (a 1)
  | 0, 3, 5 => (a 0) * (a 4) + (a 0) * (a 2) - (a 0) ^ 2
  | 0, 4, 0 => (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - 2 * (a 1) * (a 3) - 2 * (a 0) * (a 5)
  | 0, 4, 1 => (a 3) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - 2 * (a 0) * (a 3)
  | 0, 4, 2 => -(a 3) ^ 2 + (a 1) * (a 3) + (a 0) * (a 3)
  | 0, 4, 3 => -2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - 2 * (a 0) * (a 1)
  | 0, 4, 4 => (a 1) * (a 3) - (a 1) ^ 2 + (a 0) * (a 1)
  | 0, 4, 5 => (a 0) * (a 3) + (a 0) * (a 1) - (a 0) ^ 2
  | 1, 0, 0 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5)
  | 1, 0, 1 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4)
  | 1, 0, 2 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2
  | 1, 0, 3 => -2 * (a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5)
  | 1, 0, 4 => -2 * (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
  | 1, 0, 5 => -2 * (a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3)
  | 1, 1, 3 => -2 * (a 5) - 2 * (a 4) + 2 * (a 3)
  | 1, 1, 4 => -2 * (a 5) + 2 * (a 4) - 2 * (a 3)
  | 1, 1, 5 => 2 * (a 5) - 2 * (a 4) - 2 * (a 3)
  | 1, 2, 0 => -2 * (a 5)
  | 1, 2, 1 => (a 5) + (a 4) - (a 3)
  | 1, 2, 2 => (a 5) - (a 4) + (a 3)
  | 1, 2, 3 => (a 5) + (a 2) - (a 1)
  | 1, 2, 4 => (a 5) - (a 2) + (a 1)
  | 1, 2, 5 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
  | 1, 3, 0 => (a 5) + (a 4) - (a 3)
  | 1, 3, 1 => -2 * (a 4)
  | 1, 3, 2 => -(a 5) + (a 4) + (a 3)
  | 1, 3, 3 => (a 4) + (a 2) - (a 0)
  | 1, 3, 4 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
  | 1, 3, 5 => (a 4) - (a 2) + (a 0)
  | 1, 4, 0 => (a 5) - (a 4) + (a 3)
  | 1, 4, 1 => -(a 5) + (a 4) + (a 3)
  | 1, 4, 2 => -2 * (a 3)
  | 1, 4, 3 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
  | 1, 4, 4 => (a 3) + (a 1) - (a 0)
  | 1, 4, 5 => (a 3) - (a 1) + (a 0)
  | 2, 0, 0 => -(a 5) ^ 2 + (a 2) * (a 5) + (a 1) * (a 5)
  | 2, 0, 1 => (a 4) * (a 5) - 2 * (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5)
  | 2, 0, 2 => (a 3) * (a 5) - 2 * (a 2) * (a 3) - 2 * (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5)
  | 2, 0, 3 => (a 2) * (a 5) - (a 2) ^ 2 + (a 1) * (a 2)
  | 2, 0, 4 => (a 1) * (a 5) + (a 1) * (a 2) - (a 1) ^ 2
  | 2, 0, 5 => (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 2) + (a 0) * (a 1)
  | 2, 1, 0 => -2 * (a 5)
  | 2, 1, 1 => (a 5) + (a 4) - (a 3)
  | 2, 1, 2 => (a 5) - (a 4) + (a 3)
  | 2, 1, 3 => (a 5) + (a 2) - (a 1)
  | 2, 1, 4 => (a 5) - (a 2) + (a 1)
  | 2, 1, 5 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
  | 2, 2, 1 => -2 * (a 5) - 2 * (a 2) + 2 * (a 1)
  | 2, 2, 2 => -2 * (a 5) + 2 * (a 2) - 2 * (a 1)
  | 2, 2, 5 => 2 * (a 5) - 2 * (a 2) - 2 * (a 1)
  | 2, 3, 0 => (a 5) + (a 2) - (a 1)
  | 2, 3, 1 => (a 4) + (a 2) - (a 0)
  | 2, 3, 2 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
  | 2, 3, 3 => -2 * (a 2)
  | 2, 3, 4 => -(a 5) + (a 2) + (a 1)
  | 2, 3, 5 => -(a 4) + (a 2) + (a 0)
  | 2, 4, 0 => (a 5) - (a 2) + (a 1)
  | 2, 4, 1 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
  | 2, 4, 2 => (a 3) + (a 1) - (a 0)
  | 2, 4, 3 => -(a 5) + (a 2) + (a 1)
  | 2, 4, 4 => -2 * (a 1)
  | 2, 4, 5 => -(a 3) + (a 1) + (a 0)
  | 3, 0, 0 => (a 4) * (a 5) + (a 2) * (a 5) - 2 * (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - 2 * (a 0) * (a 5)
  | 3, 0, 1 => -(a 4) ^ 2 + (a 2) * (a 4) + (a 0) * (a 4)
  | 3, 0, 2 => (a 3) * (a 4) - 2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 0) * (a 5) - 2 * (a 0) * (a 4) + (a 0) * (a 3)
  | 3, 0, 3 => (a 2) * (a 4) - (a 2) ^ 2 + (a 0) * (a 2)
  | 3, 0, 4 => (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) - 2 * (a 0) * (a 2) + (a 0) * (a 1)
  | 3, 0, 5 => (a 0) * (a 4) + (a 0) * (a 2) - (a 0) ^ 2
  | 3, 1, 0 => (a 5) + (a 4) - (a 3)
  | 3, 1, 1 => -2 * (a 4)
  | 3, 1, 2 => -(a 5) + (a 4) + (a 3)
  | 3, 1, 3 => (a 4) + (a 2) - (a 0)
  | 3, 1, 4 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
  | 3, 1, 5 => (a 4) - (a 2) + (a 0)
  | 3, 2, 0 => (a 5) + (a 2) - (a 1)
  | 3, 2, 1 => (a 4) + (a 2) - (a 0)
  | 3, 2, 2 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
  | 3, 2, 3 => -2 * (a 2)
  | 3, 2, 4 => -(a 5) + (a 2) + (a 1)
  | 3, 2, 5 => -(a 4) + (a 2) + (a 0)
  | 3, 3, 0 => -2 * (a 4) - 2 * (a 2) + 2 * (a 0)
  | 3, 3, 2 => -2 * (a 4) + 2 * (a 2) - 2 * (a 0)
  | 3, 3, 4 => 2 * (a 4) - 2 * (a 2) - 2 * (a 0)
  | 3, 4, 0 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
  | 3, 4, 1 => (a 4) - (a 2) + (a 0)
  | 3, 4, 2 => (a 3) - (a 1) + (a 0)
  | 3, 4, 3 => -(a 4) + (a 2) + (a 0)
  | 3, 4, 4 => -(a 3) + (a 1) + (a 0)
  | 3, 4, 5 => -2 * (a 0)
  | 4, 0, 0 => (a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - 2 * (a 1) * (a 3) - 2 * (a 0) * (a 5)
  | 4, 0, 1 => (a 3) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - 2 * (a 0) * (a 3)
  | 4, 0, 2 => -(a 3) ^ 2 + (a 1) * (a 3) + (a 0) * (a 3)
  | 4, 0, 3 => -2 * (a 2) * (a 3) + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - 2 * (a 0) * (a 1)
  | 4, 0, 4 => (a 1) * (a 3) - (a 1) ^ 2 + (a 0) * (a 1)
  | 4, 0, 5 => (a 0) * (a 3) + (a 0) * (a 1) - (a 0) ^ 2
  | 4, 1, 0 => (a 5) - (a 4) + (a 3)
  | 4, 1, 1 => -(a 5) + (a 4) + (a 3)
  | 4, 1, 2 => -2 * (a 3)
  | 4, 1, 3 => (a 5) + (a 4) - 2 * (a 3) - 2 * (a 2) + (a 1) + (a 0)
  | 4, 1, 4 => (a 3) + (a 1) - (a 0)
  | 4, 1, 5 => (a 3) - (a 1) + (a 0)
  | 4, 2, 0 => (a 5) - (a 2) + (a 1)
  | 4, 2, 1 => (a 5) - 2 * (a 4) + (a 3) + (a 2) - 2 * (a 1) + (a 0)
  | 4, 2, 2 => (a 3) + (a 1) - (a 0)
  | 4, 2, 3 => -(a 5) + (a 2) + (a 1)
  | 4, 2, 4 => -2 * (a 1)
  | 4, 2, 5 => -(a 3) + (a 1) + (a 0)
  | 4, 3, 0 => -2 * (a 5) + (a 4) + (a 3) + (a 2) + (a 1) - 2 * (a 0)
  | 4, 3, 1 => (a 4) - (a 2) + (a 0)
  | 4, 3, 2 => (a 3) - (a 1) + (a 0)
  | 4, 3, 3 => -(a 4) + (a 2) + (a 0)
  | 4, 3, 4 => -(a 3) + (a 1) + (a 0)
  | 4, 3, 5 => -2 * (a 0)
  | 4, 4, 0 => -2 * (a 3) - 2 * (a 1) + 2 * (a 0)
  | 4, 4, 1 => -2 * (a 3) + 2 * (a 1) - 2 * (a 0)
  | 4, 4, 3 => 2 * (a 3) - 2 * (a 1) - 2 * (a 0)
  | _, _, _ => 0
THEOREM hasDerivAt_cmCofactor3Poly_34_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean
hasDerivAt_cmCofactor3Poly_34_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean:985 
/-- Closed-form coordinate derivative of the `(3,4)` cofactor polynomial. -/
theorem hasDerivAt_cmCofactor3Poly_34_along_coord
    (k : Fin 6) (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t))
      (cmCofactorPartial 3 4 k a) (a k) := by
  have hfun :
      (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t)) =
        (fun t : ℝ => cmCofactor3Poly 3 4 a
          + cmCofactorPartial 3 4 k a * (t - a k)
          + (if k = 0 then -1 else 0) * (t - a k) ^ 2
          + 0 * (t - a k) ^ 3) := by
    funext t
    have h := cmCofactor3Poly_34_update_polyform a k (t - a k)
    have hbase : a k + (t - a k) = t := by ring
    rw [hbase] at h
    simpa using h
  rw [hfun]
  exact hasDerivAt_shifted_cubic (cmCofactor3Poly 3 4 a)
    (cmCofactorPartial 3 4 k a) (if k = 0 then -1 else 0) 0 (a k)

What this page does not claim

The theorem does not claim differentiability with respect to all six edges at once. It does not provide a geometric interpretation of the derivative. It does not state any property about the tetrahedron's volume.

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/CofactorPolynomial.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND