Geometry Cofactor Derivatives Dihedral Cofactor Product Poly Ne Zero Of Non Dege

A safe denominator

In Euclidean geometry, a tetrahedron is a solid with four triangular faces. A non-degenerate tetrahedron is one whose four vertices are not all in a single plane; it has genuine volume. For such a tetrahedron, one can form a 5 by 5 matrix from its six squared edge lengths, and the Cayley-Menger cofactors of that matrix encode information about the tetrahedron's geometry, including the cosines of its dihedral angles, the angles between adjacent faces.

The declaration dihedralCofactorProductPoly_ne_zero_of_nonDegenerate is a theorem in the framework's machine-checked library of formal theorems. It states: for any non-degenerate tetrahedron and any choice of one of its six edges, a certain product of two diagonal Cayley-Menger cofactors, one for each of the two vertices opposite that edge, is not zero. The proof is short: a companion theorem shows this product is strictly positive, and a positive real number is never zero. The practical effect is that this product can safely appear in a denominator, so the derivative formulas built on it are well-defined for every non-degenerate tetrahedron.

The theorem is one step in a larger calculus layer. The library defines the derivative of the squared cosine of a dihedral angle with respect to a change in one edge length. That derivative is a quotient whose denominator involves the same cofactor product. Without the non-zero guarantee, the quotient would be undefined for some tetrahedra, and the whole derivative apparatus would have a hole. The theorem closes that hole for all non-degenerate tetrahedra at once.

What the theorem does not claim is just as important. It does not say the cofactor product is positive for degenerate tetrahedra, those with zero volume; for those, the product can vanish. It does not compute the actual value of any derivative, only the condition that keeps the derivative formulas meaningful. And it says nothing about the physical meaning of the cofactors in any broader theory; it is a purely geometric and algebraic statement about real numbers attached to a tetrahedron.

theorem dihedralCofactorProductPoly_ne_zero_of_nonDegenerate
    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
    dihedralCofactorProductPoly T.sqEdge e ≠ 0 :=
  ne_of_gt (dihedralCofactorProductPoly_pos_of_nonDegenerate T e)

/-- Nondegenerate tetrahedra have positive polynomial cofactor denominator
products for every dihedral edge. -/
theorem dihedralCofactorProductPoly_pos_of_nonDegenerate
    (T : ReggeRigorousFoundation.NonDegenerateTet) (e : Fin 6) :
    0 < dihedralCofactorProductPoly T.sqEdge e := by
  have hdisc := dihedralCofactorPoly_discriminant_eq T.sqEdge e
  have hdisc' :
      dihedralCofactorProductPoly T.sqEdge e -
          dihedralCofactorNumeratorPoly T.sqEdge e ^ 2 =
        2 * cm3 T.sqEdge * T.sqEdge e := by
    simpa [dihedralCofactorProductPoly, dihedralCofactorNumeratorPoly] using hdisc
  have hpos : 0 < 2 * cm3 T.sqEdge * T.sqEdge e := by
    nlinarith [T.cm_pos, T.sqEdge_pos e]
  have hsq : 0 ≤ dihedralCofactorNumeratorPoly T.sqEdge e ^ 2 := sq_nonneg _
  nlinarith

/-- Polynomial-cofactor closed-form derivative of the cofactor-ratio cosine. -/
def dihedralCos3SqPolyClosedFormDeriv (a : SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
  let p := (oppositeCMVertices e).1
  let q := (oppositeCMVertices e).2
  (cmCofactorPartial p q k a * dihedralDenom3Poly a e -
      cmCofactor3Poly p q a * dihedralDenom3PolyClosedDerivValue a e k) /
    (dihedralDenom3Poly a e) ^ 2

What this page does not claim

The theorem does not cover degenerate tetrahedra, where the cofactor product can be zero. The theorem does not compute any derivative value, only the condition that keeps derivative formulas defined. The theorem makes no statement about the physical interpretation of the cofactors in any broader theory.

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: