Geometry Dihedral Cayley Menger Dihedral Cos3 Regular Unit

The cofactor formula

A tetrahedron has six edges, and each pair of faces meets at a dihedral angle. For a regular tetrahedron, all six dihedral angles are equal, and their cosine is exactly 1/3, which corresponds to an angle of about 70.53 degrees. This value is a classical fact of solid geometry, known since antiquity through the study of Platonic solids.

The Cayley-Menger determinant is a classical tool that computes the volume of a simplex from its edge lengths alone. The cofactor formula for dihedral angles extracts the angle at each edge from the same edge-length data, without ever constructing the tetrahedron in coordinates. For a regular tetrahedron with unit edges, substituting the edge lengths into the cofactor formula yields cos θ = 1/3 for every edge.

In Recognition Science, the machine-checked library of formal theorems makes this substitution explicit. Its declaration dihedralCos3_regularUnit proves that the cofactor formula, applied to the regular unit tetrahedron, gives the cosine 1/3 at every edge. The proof proceeds by checking the six cofactor values directly: the off-diagonal cofactors are all 1, and the diagonal cofactors are all -3, so the quotient 1 / sqrt((-3)(-3)) = 1/3 follows. This is a theorem in the framework's library, not an assumption, and it agrees with the existing regular-tetrahedron angle API.

The declaration does not claim that the cofactor formula is the only way to compute dihedral angles, nor that it applies beyond tetrahedra. It does not assert anything about the physical meaning of the angle, and it does not derive the value 1/3 from recognition costs or the forcing chain. The result is purely geometric: a standard formula, checked for one specific regular case.

What the theorem changes is practical: downstream work can rely on the cofactor formula for the regular tetrahedron without repeating an expensive determinant expansion. The check is isolated once, and the value 1/3 is available as a proved fact for any module that needs it.

/-- 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 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 cofactor formula is not proved to be the only method for computing dihedral angles. The value 1/3 is not derived from recognition costs or any framework-specific principle. The theorem does not apply to tetrahedra with non-unit edge lengths.

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: