Geometry Affine Indep Interior Geometric Dihedral Cos Strict Interior Of Affine

Strict dihedral angles

A dihedral angle is the angle between two faces of a solid, measured along their shared edge. In a tetrahedron, the shape with four triangular faces, each of its six edges is shared by two faces, so each edge carries one dihedral angle. The cosine of that angle is the normalized dot product of the two face normals, the perpendicular vectors that define each face's orientation. For a flat or degenerate solid, a face normal can vanish or two normals can align, pushing the cosine to the endpoints -1 or 1. The classical fact at issue is that a genuinely three-dimensional, non-flat tetrahedron never suffers that collapse.

The machine-checked library of formal theorems proves exactly this strict interior property. Its declaration geometricDihedralCos_strict_interior_of_affineIndependent states that for any realized tetrahedron whose four vertices are affinely independent, meaning they do not lie in a common plane, the cosine of every dihedral angle satisfies -1 < cos < 1. The proof reduces the geometry to linear algebra: affine independence forces the two adjacent face normals to be linearly independent, and two independent vectors cannot have a normalized dot product of magnitude 1. That magnitude would require the vectors to be parallel, which independence forbids. The same argument also yields the strict interior bound for the squared-edge dihedral cosine used in the Regge closure program.

In Recognition Science, this theorem supplies the strict interior step needed for the Regge closure program, a computational scheme that reconstructs a curved spacetime from flat tetrahedral pieces. The framework models the classical geometry and then proves the endpoint exclusion as a formal theorem. What the theorem does not claim is any particular value for any dihedral angle, any statement about angles in degenerate or flat tetrahedra, or any physical law about gravity or spacetime. It establishes only the strict inequality, a necessary condition for the Regge program to proceed without endpoint singularities.

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

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

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

What this page does not claim

No particular dihedral angle value is computed or asserted. No claim is made about degenerate or flat tetrahedra, where the cosine can reach the endpoints. No physical law about gravity or spacetime is derived from this theorem alone.

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: