Geometry Cofactor Polynomial Has Deriv At Cm Cofactor3 Poly Along Coord

The derivative theorem

The Cayley-Menger determinant is a formula that decides whether six lengths can be the edges of a tetrahedron. Its cofactors, the signed minors of the associated 5 by 5 matrix, appear in formulas for dihedral angles. A machine-checked library of formal theorems expands each tetrahedral cofactor into an explicit polynomial in the six squared edge lengths, and then proves that each such polynomial is differentiable along any one coordinate.

The statement hasDerivAt_cmCofactor3Poly_along_coord is a theorem. It says that for any row and column of the cofactor matrix, and for any of the six edge coordinates, the polynomial changes smoothly when that single edge length is varied, and its derivative is exactly the separately defined partial derivative cmCofactorPartial. The derivative is evaluated at the current value of that edge length. This is a local statement: it holds at every point in the space of squared edge lengths, with no exceptional cases.

The practical content is that downstream dihedral-angle calculus can refer to named polynomial partials instead of opaque derivative terms. A later theorem, hasDerivAt_cmCofactor3Poly_34_along_coord, is the same statement specialized to the (3,4) entry. The general theorem subsumes the specialized one, and the library keeps both.

The theorem does not claim that the cofactor polynomials are globally invertible, nor that the derivative is nonzero anywhere. It does not assert that the edge lengths come from an actual tetrahedron; the polynomial is defined for all real inputs. It also does not claim that the partial derivative has a closed form in elementary functions, only that it is a well-defined real number at every point.

/-- Closed-form coordinate derivative of every cofactor polynomial. -/
theorem hasDerivAt_cmCofactor3Poly_along_coord
    (r c : Fin 5) (k : Fin 6) (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cmCofactor3Poly r c (Function.update a k t))
      (cmCofactorPartial r c k a) (a k) := by
  have hfun :
      (fun t : ℝ => cmCofactor3Poly r c (Function.update a k t)) =
        (fun t : ℝ => cmCofactor3Poly r c a
          + cmCofactorPartial r c k a * (t - a k)
          + cmCofactorQuadraticCoeff r c k a * (t - a k) ^ 2
          + 0 * (t - a k) ^ 3) := by
    funext t
    have h := cmCofactor3Poly_update_polyform r c 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 r c a)
    (cmCofactorPartial r c k a) (cmCofactorQuadraticCoeff r c k a) 0 (a k)

/-- 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 the cofactor polynomials are invertible or that their derivatives are nonzero. It does not assert the edge lengths come from an actual tetrahedron. It does not claim the partial derivative has a closed form in elementary functions.

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: