Geometry Affine Indep Interior Dihedral Cos3 Sq Strict Interior Of Face Normals

A strict angle theorem

A dihedral angle is the angle between two flat faces that meet along an edge, like the opening of a book along its spine. In a tetrahedron, a pyramid with four triangular faces, each of its six edges is shared by two faces, so it has six dihedral angles. A classical fact, proved in Euclid's spirit and now verified by a machine-checked library of formal theorems, is that in any genuinely three-dimensional tetrahedron, meaning one whose four corners do not all lie in a single plane, every dihedral angle is strictly between 0 and 180 degrees. Its cosine is therefore strictly between -1 and 1, never equal to either endpoint. An angle of 0 or 180 degrees would mean the two faces lie flat against each other, which is impossible for a solid shape.

The framework's library proves this through a chain of geometric facts. The key step is that the two face normals, the arrows perpendicular to each face, cannot be parallel when the tetrahedron is non-degenerate. If they were parallel, the faces would be coplanar, and the shape would collapse. The theorem establishes that these two normals are linearly independent, meaning neither is a scalar multiple of the other. From that independence, the normalized dot product of the normals, which is exactly the cosine of the dihedral angle, must be strictly between -1 and 1 by the Cauchy-Schwarz inequality. The library formalizes this argument in the declaration dihedralCos3Sq_strict_interior_of_faceNormals_independent, which states that given two linearly independent adjacent face normals, the cosine of the dihedral angle they define is strictly inside the open interval (-1, 1).

This result is not a new physical law or a claim about the nature of space. It is a precise, self-contained statement in Euclidean geometry, verified by a proof assistant. The theorem does not say that any particular tetrahedron exists, nor does it assign numerical values to any angles. It only guarantees a strict inequality for any non-degenerate tetrahedron. It also does not address degenerate cases where the tetrahedron is flat; those are excluded by the hypothesis of affine independence. The value of the theorem is architectural: it provides a clean, machine-checked foundation for later steps in the framework's Regge calculus program, where dihedral angles feed into discrete gravity calculations. By ensuring the cosine never hits an endpoint, the library removes a class of edge cases that would otherwise complicate downstream proofs.

In plain terms, the declaration is a rigorous guarantee of a basic geometric intuition: a solid tetrahedron cannot have a flat dihedral angle. This fact, long known and used informally, is now locked into a formal system where every step is checked by the kernel. The consequence for the framework is that all six dihedral angles of any non-degenerate tetrahedron are safely in the open range, allowing subsequent calculus and numerical work to proceed without special handling of degenerate endpoints. This is a small but essential brick in the larger edifice of the framework's geometric foundations.

/-- Strict interior transferred to the Cayley-Menger cofactor cosine for a
realized tetrahedron. -/
theorem dihedralCos3Sq_strict_interior_of_faceNormals_independent
    (T : RealizedTet) (e : Fin 6)
    (hlin : AdjacentFaceNormalsIndependent T e) :
    -1 < dihedralCos3Sq (sqEdgeOfPoints T) e ∧
      dihedralCos3Sq (sqEdgeOfPoints T) e < 1 := by
  rw [← geometricDihedralCos_eq_cmCofactorRatio T e]
  exact geometricDihedralCos_strict_interior_of_faceNormals_independent T e hlin

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

What this page does not claim

This answer does not claim that the theorem assigns any numerical value to any specific dihedral angle. This answer does not claim that the theorem applies to degenerate tetrahedra where the vertices are coplanar. This answer does not claim that the framework derives any physical law from this geometric fact.

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: