Geometry Affine Indep Interior

Dihedral angles and nondegenerate tetrahedra

A tetrahedron is a pyramid with a triangular base, four vertices, and four triangular faces. Two faces that share an edge meet along that line, and the angle between them is called a dihedral angle. In a nondegenerate tetrahedron, one where the four vertices do not all lie in a single plane, this angle is always strictly between 0 and 180 degrees. It can be very small or very close to flat, but it can never equal 0 or 180 degrees, because either endpoint would mean the two faces lie in the same plane, collapsing the tetrahedron into a flat shape. This fact is a basic property of solid geometry, and it is the starting point for the main result.

The module AffineIndepInterior proves this strict interior property in a way that is independent of any particular coordinate system. Its key insight is to look at the normal vectors of the two adjacent faces: the vectors pointing straight out of each face. If these two normals are linearly independent, meaning neither is a scalar multiple of the other, then the cosine of the dihedral angle cannot be exactly 1 or -1. The proof shows that the normalized dot product of two linearly independent vectors is always strictly between -1 and 1. This is a purely linear algebra statement, with no reference to tetrahedra at all, and it forms the analytic core of the proof.

The remaining work is to connect this linear algebra fact back to geometry. The module proves that, for a nondegenerate tetrahedron, the normals of any two adjacent faces are always linearly independent. It does this by showing that the cross product of these two normals is a nonzero scalar multiple of the shared edge vector, and that this scalar is the triple product of three edge vectors, which is nonzero precisely when the tetrahedron is nondegenerate. This chain of reasoning establishes the main theorem: for any realized nondegenerate tetrahedron, the cosine of any dihedral angle lies strictly between -1 and 1.

In Recognition Science, this result is a necessary step in the Regge closure program, which builds a discrete model of spacetime from tetrahedral building blocks. The strict interior property ensures that the dihedral angle data is well-defined and can be used in downstream calculus without hitting boundary cases. The contribution here is to remove the previous reliance on arccos endpoint inputs, making the geometric reduction from affine independence to normal independence explicit and machine-checked.

The practical consequence is that any nondegenerate tetrahedron, no matter how skewed, has dihedral angles that are always proper interior angles. This gives a clean foundation for computing with these shapes in the framework's library of formal theorems.

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

/-- The normalized dot product of two coordinate vectors is not `1` when
the vectors are linearly independent. -/
theorem dot_div_sqrt_ne_one_of_linearIndependent
    {u v : Fin 3 → ℝ} (hlin : LinearIndependent ℝ ![u, v]) :
    (u ⬝ᵥ v) / Real.sqrt ((u ⬝ᵥ u) * (v ⬝ᵥ v)) ≠ 1 := by
  intro h
  have hE :
      inner ℝ (toEuclidean3 u) (toEuclidean3 v) /
        (‖toEuclidean3 u‖ * ‖toEuclidean3 v‖) = 1 := by
    simpa [inner_toEuclidean3, sqrt_dot_self_mul_self_eq_norm_mul_norm] using h
  rcases (real_inner_div_norm_mul_norm_eq_one_iff
      (toEuclidean3 u) (toEuclidean3 v)).1 hE with ⟨huE, r, hr, hvE⟩
  have hu : u ≠ 0 := by
    intro hu0
    apply huE
    unfold toEuclidean3
    simp [hu0]
  have hv : v = r • u := smul_of_toEuclidean3_smul hvE
  exact ((LinearIndependent.pair_iff' hu).1 hlin r) hv.symm

/-- The normalized dot product of two coordinate vectors is not `-1` when
the vectors are linearly independent. -/
theorem dot_div_sqrt_ne_neg_one_of_linearIndependent
    {u v : Fin 3 → ℝ} (hlin : LinearIndependent ℝ ![u, v]) :
    (u ⬝ᵥ v) / Real.sqrt ((u ⬝ᵥ u) * (v ⬝ᵥ v)) ≠ -1 := by
  intro h
  have hE :
      inner ℝ (toEuclidean3 u) (toEuclidean3 v) /
        (‖toEuclidean3 u‖ * ‖toEuclidean3 v‖) = -1 := by
    simpa [inner_toEuclidean3, sqrt_dot_self_mul_self_eq_norm_mul_norm] using h
  rcases (real_inner_div_norm_mul_norm_eq_neg_one_iff
      (toEuclidean3 u) (toEuclidean3 v)).1 hE with ⟨huE, r, hr, hvE⟩
  have hu : u ≠ 0 := by
    intro hu0
    apply huE
    unfold toEuclidean3
    simp [hu0]
  have hv : v = r • u := smul_of_toEuclidean3_smul hvE
  exact ((LinearIndependent.pair_iff' hu).1 hlin r) hv.symm

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

/-- Adjacent tetrahedral face normals have the shared-edge cross-product
normal form edge-by-edge. -/
theorem adjacentFaceNormals_cross_eq_triple_smul_edge
    (T : RealizedTet) (e : Fin 6) :
    (adjacentFaceNormals T e).1 ⨯₃ (adjacentFaceNormals T e).2 =
      let edge := edgeVertices3 e
      let opp := adjacentFaceOppositeVertices e
      (coordEdgeVector T edge.1 edge.2 ⬝ᵥ
          coordEdgeVector T edge.1 opp.1 ⨯₃ coordEdgeVector T edge.1 opp.2) •
        coordEdgeVector T edge.1 edge.2 := by
  unfold adjacentFaceNormals faceNormal
  dsimp
  exact shared_edge_face_normals_cross _ _ _

What this page does not claim

This module does not prove that any particular physical tetrahedron exists. This module does not derive the value of any dihedral angle, only its strict interior range. This module does not address the physical bridge from recognition events to geometric realization.

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: