Geometry Affine Indep Interior Dihedral Cos3 Sq Strict Interior Of Affine Indepe

The strict interior claim

A dihedral angle is the angle between two faces of a polyhedron, measured along their shared edge. For a tetrahedron, the four triangular faces meet along six edges, so there are six dihedral angles. The cosine of such an angle is a number between -1 and 1, where -1 would mean the faces fold flat against each other and 1 would mean they lie in the same plane. The declaration dihedralCos3Sq_strict_interior_of_affineIndependent proves that for any non-degenerate tetrahedron, each of these six cosines is strictly between -1 and 1, never equal to either endpoint.

The proof rests on a geometric fact about the tetrahedron's vertices. A tetrahedron is affinely independent when its four points are not all contained in a single plane, which is exactly what it means to be a genuine three-dimensional shape rather than a flat one. From this condition, the framework's machine-checked library of formal theorems derives that the normals to any two adjacent faces are linearly independent. The normalized dot product of two such vectors, which is the cosine of the dihedral angle, then cannot be ±1, because that would require the vectors to be parallel. The theorem thus converts a statement about points into a statement about angles.

This result is a stepping stone in a larger program to reconstruct the geometry of a tetrahedron from its squared edge lengths, a method associated with the Regge calculus of discrete gravity. The strict inequality ensures that the angle data can be used to recover the shape without hitting a degenerate case where the formulas become singular. The declaration does not itself compute any specific angle value, nor does it claim that the tetrahedron is regular or that any particular angle has a particular measure. It only guarantees the safe range for all six angles.

In Recognition Science, this theorem is one of the building blocks for a discrete model of spacetime, where the ledger of recognition events is encoded in the geometry of simplices. The strict interior result is what allows the framework to move from squared edge lengths to angle data without ambiguity. It is a purely mathematical fact, proved within the framework's library, and it does not by itself establish any physical law or any claim about the nature of space.

/-- Affine independence of the realized tetrahedron gives strict interior for
the Cayley-Menger cofactor cosine at every edge. -/
theorem dihedralCos3Sq_strict_interior_of_affineIndependent
    (T : RealizedTet) (e : Fin 6) :
    -1 < dihedralCos3Sq (sqEdgeOfPoints T) e ∧
      dihedralCos3Sq (sqEdgeOfPoints T) e < 1 :=
  dihedralCos3Sq_strict_interior_of_faceNormals_independent T e
    (adjacentFaceNormalsIndependent_of_affineIndependent T e)

/-- 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

What this page does not claim

The declaration does not compute any specific dihedral angle value. It does not claim the tetrahedron is regular or that any angle has a particular measure. It does not establish any physical law or claim about the nature of space.

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: