Geometry Affine Indep Interior Face Normal Ne Zero Of Edge Vectors Linear Indepe

A face normal that cannot vanish

A tetrahedron is a pyramid with four triangular faces. Each face has a normal vector, a line pointing straight out from the face, perpendicular to its surface. The declaration faceNormal_ne_zero_of_edgeVectors_linearIndependent states a geometric fact: if two edge vectors that share a vertex are linearly independent, meaning they do not lie on the same line, then the normal vector of the face they span is not the zero vector. A zero normal would mean the face had no well-defined direction, which would make angles involving that face impossible to compute.

The theorem relies on a standard algebraic identity. In three dimensions, the cross product of two vectors is zero exactly when the vectors are linearly dependent. The normal vector is defined as the cross product of the two edge vectors. Therefore, if the edge vectors are linearly independent, their cross product, and hence the normal, cannot be zero. This is a direct application of the classical relationship between the cross product and linear independence, not a new physical principle.

This result is a stepping stone in a larger program. The machine-checked library of formal theorems uses it to show that in a non-degenerate tetrahedron, adjacent face normals are also independent, and that the cosine of a dihedral angle falls strictly between -1 and 1. That strict inequality is what makes the angle well-defined and not a degenerate endpoint. The theorem itself only establishes the non-zero normal; the further consequences are separate results built on top of it.

In Recognition Science, this theorem is part of the framework's geometric foundations, but it does not depend on any Recognition Science-specific axioms. It is a theorem about Euclidean geometry and linear algebra, proved within the framework's library. The framework uses this result to support its treatment of tetrahedral geometry, but the mathematical content stands on its own as a fact about ordinary three-dimensional space.

/-- A face normal is nonzero whenever the two edge vectors spanning the face
are linearly independent. -/
theorem faceNormal_ne_zero_of_edgeVectors_linearIndependent
    (T : RealizedTet) (a b c : Fin 4)
    (hlin : LinearIndependent ℝ ![coordEdgeVector T a b, coordEdgeVector T a c]) :
    faceNormal T a b c ≠ 0 := by
  unfold faceNormal
  exact (crossProduct_ne_zero_iff_linearIndependent).2 hlin

/-- A face normal is nonzero whenever the two edge vectors spanning the face
are linearly independent. -/
theorem faceNormal_ne_zero_of_edgeVectors_linearIndependent
    (T : RealizedTet) (a b c : Fin 4)
    (hlin : LinearIndependent ℝ ![coordEdgeVector T a b, coordEdgeVector T a c]) :
    faceNormal T a b c ≠ 0 := by
  unfold faceNormal
  exact (crossProduct_ne_zero_iff_linearIndependent).2 hlin

/-- 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 claim that the tetrahedron is non-degenerate; it only applies when the edge vectors are already known to be independent. The theorem does not establish the value of any dihedral angle, only that the cosine lies strictly between -1 and 1. The theorem does not depend on any Recognition Science-specific axiom; it is a fact of ordinary Euclidean geometry.

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: