Geometry Cofactor Derivatives Dihedral Denom3 Poly Pos Of Non Degenerate

The denominator's positivity

In the geometry of a tetrahedron, the dihedral angle between two faces is often computed from a formula involving a square root. The expression under that root, or the denominator of a related ratio, must not be zero or negative for the formula to make sense. The declaration dihedralDenom3Poly_pos_of_nonDegenerate is a machine-checked theorem stating that this denominator is strictly positive whenever the tetrahedron is non-degenerate, meaning its four vertices are not coplanar and no edge length is zero.

The denominator in question is built from Cayley-Menger cofactors, which are polynomial expressions in the squared edge lengths that appear in formulas for volumes and angles. The theorem proves positivity of the square root of a product of two such cofactors, each associated with a pair of opposite vertices. Because the product is shown to be positive, its square root is well-defined and non-zero, which is exactly the condition needed for division in formulas like the cosine of a dihedral angle.

This result is part of a larger calculus layer in the framework's machine-checked library of formal theorems, where derivative formulas for these geometric quantities are being developed. The positivity theorem is a foundational step: it ensures that later expressions involving the denominator, such as derivatives of the dihedral cosine, are valid without exceptional cases. It also implies the denominator is never zero, a fact stated separately as dihedralDenom3Poly_ne_zero_of_nonDegenerate.

What this theorem does not claim is any specific numerical value for the denominator, nor does it say anything about degenerate tetrahedra, where the positivity can fail. It also does not by itself establish the full derivative formula for the dihedral cosine; it only supplies one of the ingredients that such a formula requires. The theorem is a precise, narrow guarantee about a geometric expression, not a statement about the physical meaning of dihedral angles or about any broader theory of recognition.

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

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

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 theorem does not assign a numerical value to the denominator. This theorem does not cover degenerate tetrahedra, where the denominator can vanish. This theorem does not by itself prove the full derivative formula for the dihedral cosine.

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: