Geometry Dihedral Cofactor Formula Cm Cofactor3 Edge1 Diag Product Eq Sixteen De

The sixteen-times denominator identity

A tetrahedron has four triangular faces, and any two faces meet along an edge. The angle between those two faces is called a dihedral angle. One way to compute it is to take the two face normals, the perpendicular vectors to each face, and look at their dot product divided by the product of their lengths. That ratio is the cosine of the dihedral angle, a number between -1 and 1.

The declaration cmCofactor3_edge1_diag_product_eq_sixteen_denomSq is a theorem in the framework's machine-checked library of formal theorems. It states that, for any realized tetrahedron, the product of two specific cofactors of the squared-edge matrix equals sixteen times the squared denominator of the geometric cosine formula. In symbols: cmCofactor3 (sqEdgeOfPoints T) 1 1 * cmCofactor3 (sqEdgeOfPoints T) 2 2 = 16 * geometricDihedralDenomSq T 5. Here the cofactors come from the Cayley-Menger matrix, and the denominator is built from the face normals.

This identity is a bridge. It connects the algebraic Cayley-Menger cofactor ratio, which depends only on the six edge lengths, to the purely geometric face-normal computation. The theorem bergerCofactorFormula3 then uses this bridge to prove that the geometric cosine equals the cofactor ratio for every edge of every tetrahedron. That is the Berger cofactor formula: a classical result in tetrahedral geometry, here derived from first principles and checked by the kernel.

The identity does not claim that the cofactor product is always positive, nor that the denominator is nonzero for degenerate tetrahedra. It assumes a realized tetrahedron, meaning four points in Euclidean space with the given edge lengths. It does not extend to higher-dimensional simplices, where analogous but distinct formulas hold. It also does not assert anything about the dihedral angle itself beyond the cosine; recovering the angle requires an arccosine and a choice of branch.

In Recognition Science, this theorem is part of the geometric foundation for Regge calculus, a discrete approach to general relativity where spacetime is built from flat tetrahedral cells. The identity ensures that the geometric and algebraic descriptions of dihedral angles agree, a consistency check that any discrete gravity model needs. For a reader, the payoff is a single clean equation that ties two ways of seeing the same angle, and a proof that leaves no gap.

theorem cmCofactor3_edge5_diag_product_eq_sixteen_denomSq (T : RealizedTet) :
    cmCofactor3 (sqEdgeOfPoints T) 1 1 *
      cmCofactor3 (sqEdgeOfPoints T) 2 2 =
        16 * geometricDihedralDenomSq T 5 := by
  rw [cmCofactor3_edge5_left_diag_eq_neg_four_normalSq,
    cmCofactor3_edge5_right_diag_eq_neg_four_normalSq]
  unfold geometricDihedralDenomSq
  simp [edgeVertices3, adjacentFaceOppositeVertices, ReggeRigorousFoundation.edgeVertices]
  ring

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

What this page does not claim

This answer does not claim the cofactor product is positive for all tetrahedra. This answer does not claim the identity holds for degenerate tetrahedra or for simplices of dimension other than three. This answer does not claim the dihedral angle itself is uniquely determined by the cosine; an arccosine and branch choice are needed.

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: