Geometry Affine Indep Interior Adjacent Face Normals Independent Of Affine Indep

The strict dihedral angle

In solid geometry, a tetrahedron is a pyramid with four triangular faces. Any two faces meet along an edge, and the angle between them is called a dihedral angle. For a non-degenerate tetrahedron, one where the four corner points are not all in a single plane, this angle can never be exactly 180 degrees. If it were, the two faces would lie flat against each other, and the tetrahedron would collapse into a plane. This is a classical fact, but proving it rigorously from the definition of a tetrahedron takes care.

The Recognition Science framework's machine-checked library of formal theorems contains a proof of this fact. The key declaration, adjacentFaceNormalsIndependent_of_affineIndependent, establishes that for any non-degenerate tetrahedron, the normal vectors (the arrows pointing straight out of each face) of any two adjacent faces are linearly independent. Two vectors are linearly independent if neither is a scalar multiple of the other, meaning they point in genuinely different directions. The proof then uses this independence to show that the cosine of the dihedral angle, a number that measures the angle's size, is strictly between -1 and 1. A cosine of exactly 1 would mean a zero angle, and a cosine of -1 would mean a 180-degree angle, both of which are impossible for a non-degenerate tetrahedron.

The proof chain works by starting with the affine independence of the tetrahedron's four corner points, which is the formal way of saying they are not coplanar. From this, it derives the linear independence of the edge vectors, then the non-zero triple product of those vectors, and finally the independence of the face normals. Each step is a formal theorem, checked by the computer, with no gaps or hand-waving. This result is not just an isolated curiosity; it is a needed step in a larger program to compute the geometry of tetrahedral meshes, where knowing that dihedral angles are strictly interior avoids special cases in downstream calculations.

What this declaration does not claim is also important. It does not claim that all dihedral angles in a tetrahedron are equal, nor does it say anything about the specific size of any angle beyond ruling out the two degenerate extremes. It does not apply to degenerate tetrahedra where the points are coplanar, and it does not extend to higher-dimensional simplices or other polyhedra. The result is specific to the three-dimensional tetrahedron and its six edges, and it is a statement about the geometry of the shape itself, not about any physical property or about the Recognition Science framework's broader claims about the nature of reality.

/-- Affine independence of the tetrahedron implies adjacent face-normal
independence for every edge. -/
theorem adjacentFaceNormalsIndependent_of_affineIndependent
    (T : RealizedTet) (e : Fin 6) :
    AdjacentFaceNormalsIndependent T e := by
  have hlin := edge_opposite_coord_triple_linearIndependent T e
  have htriple := scalar_triple_ne_zero_of_linearIndependent hlin
  exact adjacentFaceNormalsIndependent_of_triple_ne_zero T e htriple

/-- Affine independence of the realized tetrahedron gives strict interior for
the geometric dihedral cosine at every edge. -/
theorem geometricDihedralCos_strict_interior_of_affineIndependent
    (T : RealizedTet) (e : Fin 6) :
    -1 < geometricDihedralCos T e ∧ geometricDihedralCos T e < 1 :=
  geometricDihedralCos_strict_interior_of_faceNormals_independent T e
    (adjacentFaceNormalsIndependent_of_affineIndependent T e)

What this page does not claim

Not a claim that all dihedral angles in a tetrahedron are equal. Not a statement about the specific size of any dihedral angle. Not a result that applies to degenerate tetrahedra or to polyhedra other than tetrahedra.

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