Geometry Cofactor Derivatives Has Deriv At Dihedral Cos3 Sq From Cofactors

The derivative theorem

In three-dimensional geometry, a tetrahedron is a solid with four triangular faces, and a dihedral angle is the angle between two faces along a shared edge. The squared cosine of that angle, written cos²θ, is a number between 0 and 1 that encodes the angle's sharpness. A natural question is: if you stretch one edge of the tetrahedron by a tiny amount, how fast does cos²θ change? The answer is a derivative, and the theorem hasDerivAt_dihedralCos3Sq_from_cofactors in the framework's machine-checked library of formal theorems proves that this derivative exists and gives its exact formula.

The theorem works with a path that changes a single edge length while the other five stay fixed. It assumes the tetrahedron is non-degenerate, meaning it has positive volume and no face collapses to a line. Under that condition, the derivative of cos²θ along the path equals a rational expression built from the derivatives of certain cofactors (signed minors of a matrix) and the denominator's value. The formula is: (num'·den − num·den') / den², which is the standard quotient rule for derivatives, applied to the ratio that defines cos²θ. The theorem confirms that this quotient rule is valid in this geometric setting, with no hidden assumptions about smoothness beyond what the cofactors provide.

The proof rests on two earlier results in the same library. The first shows that each cofactor is continuously differentiable, so its derivative exists everywhere. The second shows that the denominator, a square root of a product of cofactors, is differentiable and nonzero for non-degenerate tetrahedra. The theorem then assembles these pieces using the chain rule and the quotient rule. The final statement is a theorem, a claim proved in the machine-checked library with no axioms beyond the standard logical ones, so it is not a conjecture or an approximation.

What the theorem does not claim is important. It does not give a closed-form expression for the derivative in terms of edge lengths alone; the formula still references the cofactors and their derivatives, which are themselves defined by determinants. It does not claim that the derivative is nonzero, so it does not tell you whether cos²θ is increasing or decreasing. It also does not extend to degenerate tetrahedra, where the denominator can vanish and the derivative may blow up or fail to exist. Finally, it says nothing about the second derivative or about how cos²θ changes when multiple edges vary at once; those are separate questions that would need their own theorems.

/-- Dihedral cosine derivative from the numerator and diagonal cofactor
derivatives. -/
theorem hasDerivAt_dihedralCos3Sq_from_cofactors
    {γ : ℝ → SqEdges} {x num' pp' qq' : ℝ} (e : Fin 6)
    (hnum : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        let q := (oppositeCMVertices e).2
        cmCofactor3 (γ t) p q) num' x)
    (hpp : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        cmCofactor3 (γ t) p p) pp' x)
    (hqq : HasDerivAt
      (fun t : ℝ =>
        let q := (oppositeCMVertices e).2
        cmCofactor3 (γ t) q q) qq' x)
    (hprod_ne :
      (let p := (oppositeCMVertices e).1
       let q := (oppositeCMVertices e).2
       cmCofactor3 (γ x) p p * cmCofactor3 (γ x) q q) ≠ 0)
    (hden_ne : dihedralDenom3 (γ x) e ≠ 0) :
    HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e)
      (dihedralCos3SqDerivValue γ x num'
        (dihedralDenom3DerivValue γ x pp' qq' e) e) x := by
  refine hasDerivAt_dihedralCos3Sq_along e hnum ?_ hden_ne
  simpa [dihedralDenom3DerivValue] using
    hasDerivAt_dihedralDenom3_along e hpp hqq hprod_ne

/-- Dihedral cosine derivative from the numerator and diagonal cofactor
derivatives. -/
theorem hasDerivAt_dihedralCos3Sq_from_cofactors
    {γ : ℝ → SqEdges} {x num' pp' qq' : ℝ} (e : Fin 6)
    (hnum : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        let q := (oppositeCMVertices e).2
        cmCofactor3 (γ t) p q) num' x)
    (hpp : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        cmCofactor3 (γ t) p p) pp' x)
    (hqq : HasDerivAt
      (fun t : ℝ =>
        let q := (oppositeCMVertices e).2
        cmCofactor3 (γ t) q q) qq' x)
    (hprod_ne :
      (let p := (oppositeCMVertices e).1
       let q := (oppositeCMVertices e).2
       cmCofactor3 (γ x) p p * cmCofactor3 (γ x) q q) ≠ 0)
    (hden_ne : dihedralDenom3 (γ x) e ≠ 0) :
    HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e)
      (dihedralCos3SqDerivValue γ x num'
        (dihedralDenom3DerivValue γ x pp' qq' e) e) x := by
  refine hasDerivAt_dihedralCos3Sq_along e hnum ?_ hden_ne
  simpa [dihedralDenom3DerivValue] using
    hasDerivAt_dihedralDenom3_along e hpp hqq hprod_ne

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

What this page does not claim

The theorem does not give a closed-form expression for the derivative solely in terms of edge lengths. The theorem does not state whether the derivative is positive or negative. The theorem does not cover degenerate tetrahedra where the denominator vanishes.

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: