Geometry Dihedral Cofactor Formula Dihedral Cos3 Sq Sq Edge Of Points Interior O

The interior cosine theorem

A dihedral angle is the angle between two flat faces that meet along an edge, like the angle between two pages of an open book. In a tetrahedron, the solid with four triangular faces, each of its six edges has a dihedral angle. The cosine of that angle, a number between -1 and 1, measures how sharply the two faces fold toward each other: cosine 1 means the faces lie flat in the same plane, and cosine -1 means they fold back exactly onto each other.

The theorem dihedralCos3Sq_sqEdgeOfPoints_interior_of_ne_endpoints states that if the cosine of a dihedral angle in a tetrahedron is not equal to -1 and not equal to 1, then it lies strictly between -1 and 1. In symbols, if cos(θ) ≠ -1 and cos(θ) ≠ 1, then -1 < cos(θ) < 1. This is a statement about the geometry of a tetrahedron defined by four points in ordinary three-dimensional space, where each face is a triangle and the angle is computed from the face normals, the perpendicular vectors to each face.

The proof works by first showing that the cosine always lies in the closed interval from -1 to 1, a fact that follows from the Cauchy-Schwarz inequality applied to the face normals. The theorem then simply rules out the two endpoints: if the cosine were exactly 1 or -1, the faces would be parallel or anti-parallel, which would force the tetrahedron to collapse into a plane. The result is a clean interior property: the cosine of a genuine, non-degenerate dihedral angle is always strictly between the extremes.

This theorem is a small piece of a larger project in the machine-checked library of formal theorems. The library proves the Berger cofactor formula, which identifies this geometric cosine with a ratio of Cayley-Menger cofactors, quantities computed purely from the squared edge lengths of the tetrahedron. The interior theorem is the bridge that lets the library pass from the geometric definition of the angle to the algebraic formula, ensuring the two agree for every edge of every non-degenerate tetrahedron.

What the theorem does not claim is just as important as what it proves. It does not say that every tetrahedron has a dihedral angle whose cosine is strictly between -1 and 1; that would be false, since a flat tetrahedron has cosines equal to 1. It only says that if the cosine is not an endpoint, then it is interior. Nor does it claim anything about the size of the angle itself, only about its cosine. The theorem is a precise, narrow statement about the range of a geometric quantity, not a broad claim about all tetrahedra.

/-- Cofactor dihedral cosines of realized tetrahedra are strictly interior
once endpoint cases are excluded. -/
theorem dihedralCos3Sq_sqEdgeOfPoints_interior_of_ne_endpoints
    (T : RealizedTet) (e : Fin 6)
    (hneg : dihedralCos3Sq (sqEdgeOfPoints T) e ≠ -1)
    (hpos : dihedralCos3Sq (sqEdgeOfPoints T) e ≠ 1) :
    -1 < dihedralCos3Sq (sqEdgeOfPoints T) e ∧
      dihedralCos3Sq (sqEdgeOfPoints T) e < 1 := by
  rw [← geometricDihedralCos_eq_cmCofactorRatio T e] at hneg hpos ⊢
  exact geometricDihedralCos_interior_of_ne_endpoints T e hneg hpos

/-- Cofactor-defined dihedral cosines of realized tetrahedra lie in `[-1,1]`. -/
theorem dihedralCos3Sq_sqEdgeOfPoints_range (T : RealizedTet) (e : Fin 6) :
    -1 ≤ dihedralCos3Sq (sqEdgeOfPoints T) e ∧
      dihedralCos3Sq (sqEdgeOfPoints T) e ≤ 1 := by
  rw [← geometricDihedralCos_eq_cmCofactorRatio T e]
  exact geometricDihedralCos_range T e

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

What this page does not claim

Every tetrahedron has a dihedral angle whose cosine is strictly between -1 and 1. The theorem says anything about the size of the dihedral angle itself, only about its cosine. The theorem applies to degenerate tetrahedra, where faces lie flat or fold exactly back.

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: