Geometry Cofactor Polynomial Has Deriv At Cm Cofactor3 Along Coord

The derivative theorem

The statement begins with a familiar object from geometry: the squared distance between two points. For a tetrahedron, there are six such squared edge lengths. The Cayley-Menger matrix is a 5 by 5 table built from these six numbers, and its cofactors are the signed determinants of the 4 by 4 tables you get by deleting one row and one column. These cofactors appear in formulas for dihedral angles and other metric properties of the tetrahedron.

The theorem in question concerns one specific cofactor, the one in the third row and fourth column, and how it changes when you vary a single squared edge length while holding the other five fixed. The declaration states that this cofactor is differentiable as a function of that one variable, and that its derivative is given by a named polynomial called the partial cofactor. In symbols, if you write the cofactor as a function of the edge coordinate t, then its derivative at the point a k is exactly cmCofactorPartial 3 4 k a.

This is a technical but useful result. It converts a request like "how much does this angle-related quantity shift when I pull on this edge?" from a problem of expanding and differentiating a large polynomial into a direct lookup of a named formula. The theorem is proved in a machine-checked library of formal theorems, meaning the chain of logical steps has been verified by a computer program. The proof also covers the general case for any row and column, not just the one named in the question.

What the theorem does not claim is just as important as what it does. It does not say that the cofactor polynomial has any special geometric meaning beyond being the cofactor of the Cayley-Menger matrix. It does not assert that the derivative is nonzero, or that the function is differentiable more than once. It only establishes the first derivative exists and gives its value. The theorem also does not connect this derivative to any physical quantity or to the broader forcing chain of the Recognition Science framework; it is a standalone piece of calculus about a specific matrix.

/-- 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)

/-- 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 that the cofactor polynomial has any meaning beyond being the cofactor of the Cayley-Menger matrix. The theorem does not assert that the derivative is nonzero or that the function is differentiable more than once. The theorem does not connect this derivative to any physical quantity or to the broader forcing chain of the Recognition Science framework.

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: