Geometry Dihedral Cofactor Formula

The dihedral angle from edge lengths

A dihedral angle is the angle between two faces of a polyhedron, measured along their shared edge. For a tetrahedron, the simplest polyhedron with four triangular faces, there are six such angles, one for each edge. The classical problem is to compute these angles from the tetrahedron's shape. The shape is fully described by the six edge lengths, so the question is whether the dihedral angles can be expressed directly in terms of those lengths. The answer is yes, and the formula is known as the Cayley-Menger cofactor formula.

The formula works by building a matrix from the squared edge lengths. The cosine of the dihedral angle at a given edge is then a ratio of two cofactors of that matrix, divided by a square root of a product of diagonal cofactors. This is a purely algebraic expression, with no reference to coordinates or angles. The formula is useful because it lets you compute dihedral angles from a distance matrix alone, which is the natural data in many geometric and physical problems.

In Recognition Science, the framework's machine-checked library of formal theorems proves that this algebraic formula agrees with the geometric definition. The geometric definition is the usual one: take the two face normals, the vectors perpendicular to the faces, and compute the cosine of the angle between them via their dot product. The module DihedralCofactorFormula proves that for every edge of every realized tetrahedron, the geometric cosine equals the Cayley-Menger cofactor ratio. The main theorem, bergerCofactorFormula3, states this equality for all six edges.

The proof works by expressing the geometric quantities in terms of a Gram matrix of edge vectors, then showing that the cofactor ratio simplifies to the same expression. The library also proves that the resulting cosine values always lie between -1 and 1, which confirms they correspond to real angles. This is a foundational result: it connects the abstract algebraic structure of distance matrices to the concrete geometry of angles, a bridge that is needed for further work in the framework.

For a reader, the practical takeaway is that you can compute a tetrahedron's dihedral angles from its edge lengths alone, without ever choosing coordinates. The formula is exact and now verified by a machine-checked proof, so it can be used as a reliable building block in larger constructions.

/-- The theorem target is discharged. -/
theorem bergerCofactorFormula3 : BergerCofactorFormula3 :=
  geometricDihedralCos_eq_cmCofactorRatio

/-- Geometric dihedral cosines lie in `[-1, 1]`. -/
theorem geometricDihedralCos_range (T : RealizedTet) (e : Fin 6) :
    -1 ≤ geometricDihedralCos T e ∧ geometricDihedralCos T e ≤ 1 := by
  unfold geometricDihedralCos geometricDihedralNumerator geometricDihedralDenomSq
  dsimp
  exact abs_le.mp (abs_dot_div_sqrt_self_mul_self_le_one _ _)

What this page does not claim

This module does not derive the dihedral angle formula from the Recognition Science cost function. The formula is not claimed to be new; the module proves a known geometric identity. The proof 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/DihedralCofactorFormula.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: