Geometry Cofactor Derivatives Dihedral Denom3 Poly Ne Zero Of Non Degenerate

The denominator stays alive

A tetrahedron is the simplest solid with flat triangular faces, a pyramid on a triangular base. A non-degenerate tetrahedron is one whose four corners do not lie in a single plane; it has a genuine volume and no face collapses onto another. The declaration dihedralDenom3Poly_ne_zero_of_nonDegenerate concerns a quantity built from the tetrahedron's six edge lengths, a denominator that appears when computing how a dihedral angle, the angle between two faces along a shared edge, changes as the edge lengths vary.

The theorem states that for any non-degenerate tetrahedron, this denominator is not zero. The proof is direct: a companion result shows the denominator is in fact strictly positive, and a positive number is certainly not zero. The denominator is a square root of a product of two cofactors, quantities that arise in the Cayley-Menger formalism for distances in a simplex. The positivity result rests on the non-degeneracy condition, which rules out the degenerate cases where the geometry collapses and the denominator could vanish.

This matters because the denominator appears in the derivative formulas for the square of the cosine of a dihedral angle. A derivative formula that divides by this denominator is only meaningful when the denominator is non-zero. The theorem supplies exactly that guarantee for every non-degenerate tetrahedron, so the calculus layer for these geometric quantities is sound wherever it is applied. It is a technical but necessary condition, the kind of fact that lets a larger proof proceed without checking a special case at every step.

The declaration does not claim that the denominator is positive, only that it is non-zero; the positivity is a separate theorem. It also does not claim anything about degenerate tetrahedra, where the denominator may or may not vanish. It says nothing about the physical meaning of these quantities in the Recognition Science framework, and it does not establish any formula for the derivative itself, only the non-vanishing of a denominator that appears in such formulas.

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)

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 denominator is positive for all tetrahedra, including degenerate ones. The theorem provides a formula for the derivative of the dihedral angle cosine. The quantities involved have a specific physical interpretation in Recognition Science.

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: