Geometry Affine Indep Interior Geometric Dihedral Cos Strict Interior Of Face No

The strict interior theorem

In three-dimensional geometry, a dihedral angle is the angle between two flat faces that meet along an edge. Its cosine is a number between -1 and 1. The endpoints are degenerate cases: a cosine of 1 means the faces lie flat in the same plane, and a cosine of -1 means they fold back onto each other. A tetrahedron, the simplest solid with four triangular faces, has six edges and therefore six dihedral angles, one per edge.

The framework's machine-checked library of formal theorems proves a precise statement about these angles. The theorem geometricDihedralCos_strict_interior_of_faceNormals_independent says: if the two face normals adjacent to an edge are linearly independent, then the cosine of that dihedral angle is strictly between -1 and 1. In plain words, independence of the normals forces the angle to be a genuine interior angle, not a degenerate flat or fully folded one. The proof reduces the claim to a fact about vectors: two linearly independent vectors have a normalized dot product strictly between -1 and 1.

The theorem is a component of a larger program to give rigorous foundations for Regge calculus, a discrete approach to general relativity where spacetime is approximated by flat simplices. The declaration itself does not prove that the face normals of an arbitrary tetrahedron are independent. That independence is a separate hypothesis, supplied by the AffineIndependent field of a realized tetrahedron. A companion theorem, geometricDihedralCos_strict_interior_of_affineIndependent, supplies that hypothesis and derives the same strict interior conclusion.

The result is analytic and geometric, not physical. It makes no claim about the value of any specific dihedral angle, nor about the Regge action or any gravitational dynamics. It establishes a necessary condition for a well-defined interior angle, removing the need for special handling of arccos endpoint inputs in downstream calculus once normal independence is available.

/-- Strict interior for the geometric dihedral cosine, given linear
independence of the two adjacent face normals. -/
theorem geometricDihedralCos_strict_interior_of_faceNormals_independent
    (T : RealizedTet) (e : Fin 6)
    (hlin : AdjacentFaceNormalsIndependent T e) :
    -1 < geometricDihedralCos T e ∧ geometricDihedralCos T e < 1 := by
  refine geometricDihedralCos_interior_of_ne_endpoints T e ?_ ?_
  · unfold geometricDihedralCos geometricDihedralNumerator geometricDihedralDenomSq
    unfold AdjacentFaceNormalsIndependent adjacentFaceNormals at hlin
    dsimp at hlin ⊢
    exact dot_div_sqrt_ne_neg_one_of_linearIndependent hlin
  · unfold geometricDihedralCos geometricDihedralNumerator geometricDihedralDenomSq
    unfold AdjacentFaceNormalsIndependent adjacentFaceNormals at hlin
    dsimp at hlin ⊢
    exact dot_div_sqrt_ne_one_of_linearIndependent hlin

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

The theorem does not prove that face normals of a realized tetrahedron are independent; that is a separate hypothesis. The theorem makes no statement about the numerical value of any particular dihedral angle. The theorem does not connect dihedral angles to the framework's cost function or the forcing chain.

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: