Geometry Cofactor Derivatives Dihedral Denom3 Closed Deriv Value Eq Poly

The closed derivative identity

In the geometry of a tetrahedron, the dihedral angle between two faces is often computed through a ratio of Cayley-Menger cofactors, which are polynomial expressions built from the six edge lengths. The denominator of that ratio is the square root of a product of two such cofactors. When one edge length varies, the denominator changes, and its rate of change is a derivative that appears in formulas for how the dihedral angle responds to deformation.

The theorem dihedralDenom3ClosedDerivValue_eq_poly states that two ways of writing this derivative are identical. The first way, called the closed derivative, is defined directly from the original cofactor functions and their partial derivatives. The second way, the polynomial derivative, first rewrites each cofactor as an explicit polynomial in the edge lengths and then differentiates those polynomials. The theorem proves that for any tetrahedron and any choice of edge, the closed derivative equals the polynomial derivative. This is not an approximation or a numerical coincidence; it is an equality of real numbers, verified by a machine-checked library of formal theorems.

The proof is short. It unfolds both definitions, applies an earlier theorem that rewrites the denominator as its polynomial form, and then rewrites each cofactor using the same polynomial identity. The result is a direct symbolic equality. The theorem also comes with supporting results: the denominator is positive for non-degenerate tetrahedra, and the product inside the square root is positive as well, so the square root is well defined and the derivative expression never divides by zero in the non-degenerate case.

What the theorem does not claim is just as important. It does not assert that the derivative has any particular numerical value, nor that it is nonzero, nor that the dihedral angle itself has a closed form. It only establishes that two different symbolic expressions for the derivative agree. The theorem also does not say anything about how the derivative behaves at degenerate tetrahedra, where the denominator can vanish; those cases are excluded by the non-degeneracy condition. Finally, the theorem is about the denominator of the dihedral cosine ratio, not about the full derivative of the dihedral angle itself, which would involve additional factors from the numerator and the quotient rule.

In the Recognition Science framework, this identity is a piece of the calculus layer that supports later work on how geometric quantities change under edge-length variation. It is a proved theorem, not a model or a hypothesis, and it holds for all non-degenerate tetrahedra. The practical consequence is that any computation using the closed derivative can be replaced by the polynomial form without changing the result, which simplifies further symbolic manipulation and numerical evaluation.

theorem dihedralDenom3ClosedDerivValue_eq_poly (a : SqEdges) (e : Fin 6) (k : Fin 6) :
    dihedralDenom3ClosedDerivValue a e k =
      dihedralDenom3PolyClosedDerivValue a e k := by
  unfold dihedralDenom3ClosedDerivValue dihedralDenom3PolyClosedDerivValue
    dihedralLeftDiagClosedDeriv dihedralRightDiagClosedDeriv
  rw [dihedralDenom3_eq_poly]
  simp_rw [cmCofactor3_eq_poly]

theorem dihedralDenom3Poly_pos_of_nonDegenerate
    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
    0 < dihedralDenom3Poly T.sqEdge e := by
  unfold dihedralDenom3Poly
  rw [Real.sqrt_pos]
  simpa [dihedralCofactorProductPoly] using
    dihedralCofactorProductPoly_pos_of_nonDegenerate T e

What this page does not claim

The theorem does not give a numerical value for the derivative. The theorem does not apply to degenerate tetrahedra. The theorem does not describe the derivative of the dihedral angle itself.

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: