Geometry Dihedral Cayley Menger

The tetrahedral angle formula

The dihedral angle of a tetrahedron is the angle between two of its faces, measured along their shared edge. For a triangular pyramid, the angle between two adjacent triangular sides is like the slope of a roof meeting at a ridge. The Cayley-Menger formula is a classical result that computes volumes and angles of a simplex from nothing but its edge lengths, without ever placing it in coordinates. For a tetrahedron, this means six numbers determine all four faces and all six dihedral angles.

The formula works through a 5 by 5 matrix built from the squared edge lengths. The cofactor matrix of this Cayley-Menger matrix carries the geometric information: for an edge with two opposite vertices, the cosine of the dihedral angle at that edge equals a cofactor entry divided by the square root of the product of two diagonal cofactors. For a regular tetrahedron, where all six edges are equal, this formula yields cos θ = 1/3, corresponding to an angle of about 70.53 degrees, the standard internal dihedral angle of the regular tetrahedron.

In Recognition Science, the framework's machine-checked library of formal theorems contains a module that makes this formula precise. The module defines the vertex indexing, the opposite-vertex pairs for each edge, and the cofactor-based cosine and angle functions. It then proves, without external assumptions, that for the regular unit tetrahedron the cofactor formula gives cos θ = 1/3. A separate theorem confirms that this cofactor-defined angle agrees exactly with the existing regular-tetrahedron dihedral angle in the library's API.

The achievement is not the formula itself, which is classical, but the formal verification. The library proves the regular case by checking the cofactor values directly: off-diagonal cofactors equal 1 and diagonal cofactors equal -3 for every edge. This turns a textbook formula into a theorem with a machine-checked proof, so downstream work can rely on the angle value without redoing the determinant expansion. The regular case is the anchor; the general case, where edge lengths vary, remains a target for further formalization.

/-- The cofactor formula gives the standard regular tetrahedron value
`cos θ = 1 / 3` without external assumptions. -/
theorem dihedralCos3_regularUnit (e : Fin 6) :
    dihedralCos3 regularUnitTet e = (1 / 3 : ℝ) :=
  dihedralCos3_regularUnit_of_cofactorCheck regularUnitCofactorCheck e

/-- The cofactor angle agrees with the existing regular-tetrahedron
dihedral API without external assumptions. -/
theorem dihedralAngle3_regularUnit (e : Fin 6) :
    dihedralAngle3 regularUnitTet e = regular_tet_dihedral.theta :=
  dihedralAngle3_regularUnit_of_cofactorCheck regularUnitCofactorCheck e

/-- The regular-unit cofactor check is now a theorem, not an assumption. -/
theorem regularUnitCofactorCheck : RegularUnitCofactorCheck := by
  intro e
  fin_cases e <;>
    simp [oppositeCMVertices,
      regularUnit_cofactor_34, regularUnit_cofactor_24, regularUnit_cofactor_23,
      regularUnit_cofactor_14, regularUnit_cofactor_13, regularUnit_cofactor_12,
      regularUnit_vertex_diag_cofactor]

What this page does not claim

The general case of unequal edge lengths is not proved in this module. The Cayley-Menger determinant formula for volume is not derived here. No claim is made about the physical recognition-to-linking bridge for three dimensions.

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/DihedralCayleyMenger.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: