Geometry Cofactor Derivatives

Cofactor derivatives

In geometry, a cofactor is a signed minor of a matrix, and the Cayley-Menger matrix encodes the squared distances between points. For a tetrahedron, its cofactors carry information about the volumes and dihedral angles of the shape. The Cayley-Menger cofactor derivative is the rate at which such a cofactor changes when one edge length is varied, while the other edges stay fixed. This library in the Recognition Science framework makes that calculus layer explicit: it defines the derivative of a Cayley-Menger cofactor with respect to an edge length, and it proves the derivative exists and has the expected closed form.

The central object is the squared cosine of a dihedral angle, written as a ratio of cofactors. The library proves that this ratio, as a function of a single edge length, is differentiable, and it gives the derivative explicitly as a quotient formula. The proof works by first showing that each cofactor is continuously differentiable, then applying the standard quotient rule for derivatives. The result is a closed-form expression for the derivative of the squared cosine of a dihedral angle with respect to an edge length, valid whenever the tetrahedron is non-degenerate, meaning its volume is not zero.

The library also establishes that the denominator in these expressions, a square root of a product of two cofactors, is never zero for a non-degenerate tetrahedron. This is the key condition that makes the quotient rule applicable. The theorems are machine-checked, meaning they are verified by a computer proof assistant, so the calculus is no longer implicit but is grounded in formal proof.

In the Recognition Science framework, this library provides the analytic foundation for how geometric quantities change as edge lengths vary. It is a step toward understanding how the shape of a tetrahedron responds to deformations, which is relevant for any model that treats space as built from discrete geometric cells. The library does not yet provide the full symbolic simplifications of these derivatives, but it establishes the existence and the form of the derivatives, which is the necessary groundwork.

/-- Canonical Fréchet derivative of a Cayley-Menger cofactor. -/
def cmCofactor3FDeriv (r c : Fin 5) (a : SqEdges) : SqEdges →L[ℝ] ℝ :=
  fderiv ℝ (fun x : SqEdges => cmCofactor3 x r c) a

/-- Cofactors are differentiable everywhere because they are smooth
polynomial functions of the squared-edge coordinates. -/
theorem hasFDerivAt_cmCofactor3 (r c : Fin 5) (a : SqEdges) :
    HasFDerivAt (fun x : SqEdges => cmCofactor3 x r c)
      (cmCofactor3FDeriv r c a) a := by
  unfold cmCofactor3FDeriv
  exact ((cmCofactor3_contDiff 1 r c).differentiable_one a).hasFDerivAt

/-- Explicit coordinate derivative of the Cayley-Menger cofactor cosine. -/
theorem hasDerivAt_dihedralCos3Sq_explicit
    (a : SqEdges) (e k : Fin 6)
    (hprod_ne :
      (let p := (oppositeCMVertices e).1
       let q := (oppositeCMVertices e).2
       cmCofactor3 a p p * cmCofactor3 a q q) ≠ 0)
    (hden_ne : dihedralDenom3 a e ≠ 0) :
    HasDerivAt (fun t : ℝ => dihedralCos3Sq (Function.update a k t) e)
      (dihedralCos3SqClosedFormDeriv a e k) (a k) := by
  let p := (oppositeCMVertices e).1
  let q := (oppositeCMVertices e).2
  have hnum :
      HasDerivAt
        (fun t : ℝ =>
          let p := (oppositeCMVertices e).1
          let q := (oppositeCMVertices e).2
          cmCofactor3 (Function.update a k t) p q)
        (dihedralNumeratorClosedDeriv a e k) (a k) := by
    simpa [dihedralNumeratorClosedDeriv, p, q] using
      hasDerivAt_cmCofactor3_along_coord p q k a
  have hpp :
      HasDerivAt
        (fun t : ℝ =>
          let p := (oppositeCMVertices e).1
          cmCofactor3 (Function.update a k t) p p)
        (dihedralLeftDiagClosedDeriv a e k) (a k) := by
    simpa [dihedralLeftDiagClosedDeriv, p] using
      hasDerivAt_cmCofactor3_along_coord p p k a
  have hqq :
      HasDerivAt
        (fun t : ℝ =>
          let q := (oppositeCMVertices e).2
          cmCofactor3 (Function.update a k t) q q)
        (dihedralRightDiagClosedDeriv a e k) (a k) := by
    simpa [dihedralRightDiagClosedDeriv, q] using
      hasDerivAt_cmCofactor3_along_coord q q k a
  have hbase :
      Function.update a k (a k) = a := by
    funext i
    by_cases hi : i = k <;> simp [Function.update, hi]
  have h :=
    hasDerivAt_dihedralCos3Sq_from_cofactors
      (γ := fun t : ℝ => Function.update a k t) (x := a k)
      (num' := dihedralNumeratorClosedDeriv a e k)
      (pp' := dihedralLeftDiagClosedDeriv a e k)
      (qq' := dihedralRightDiagClosedDeriv a e k)
      e hnum hpp hqq ?_ ?_
  · simpa [dihedralCos3SqClosedFormDeriv, dihedralCos3SqDerivValue,
      dihedralDenom3ClosedDerivValue, dihedralDenom3DerivValue,
      dihedralNumeratorClosedDeriv, dihedralLeftDiagClosedDeriv,
      dihedralRightDiagClosedDeriv, hbase, p, q] using h
  · simpa [hbase, p, q] using hprod_ne
  · simpa [hbase] using hden_ne

theorem dihedralDenom3Poly_ne_zero_of_nonDegenerate
    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
    dihedralDenom3Poly T.sqEdge e ≠ 0 :=
  ne_of_gt (dihedralDenom3Poly_pos_of_nonDegenerate T e)

What this page does not claim

This library does not provide simplified symbolic expressions for the derivatives; it establishes their existence and closed form. This library does not connect cofactor derivatives to any physical law or constant in the Recognition Science framework. This library does not address the geometry of objects other than tetrahedra.

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