Geometry Affine Indep Interior Adjacent Face Normals Independent Of Triple Ne Ze

The face-normal lemma

A tetrahedron is a pyramid with four triangular faces. Take any one of its six edges. Two faces meet along that edge. Each face has a normal vector, a line perpendicular to the face. The lemma in question says these two normal vectors are linearly independent: neither is a scalar multiple of the other, so they are not parallel. The proof rests on a single condition. Let the shared edge run from vertex A to vertex B, and let the two opposite vertices be C and D. The condition is that the triple product of the edge vector AB with the two vectors AC and AD is nonzero. This triple product measures the signed volume of the parallelepiped spanned by those three vectors. A nonzero value means the three vectors are not coplanar, which is exactly what it means for the tetrahedron to be nondegenerate, not flattened into a plane.

The declaration named adjacentFaceNormalsIndependent_of_triple_ne_zero is a theorem in the framework's machine-checked library of formal theorems. It states that if that triple product is nonzero, then the two adjacent face normals are linearly independent. The proof is short and algebraic. The cross product of the two face normals equals a scalar multiple of the shared edge vector, where the scalar is precisely the triple product. Since the triple product is nonzero and the edge vector is nonzero, the cross product of the normals is nonzero, which is equivalent to their linear independence. This is the key step that lets the library conclude that the cosine of the dihedral angle, the angle between the two faces, lies strictly between -1 and 1, never reaching the endpoints that would mean the faces are folded flat onto each other.

In Recognition Science, this lemma is a brick in a larger construction. The framework models physical space through realized tetrahedra, and it needs dihedral angles to be strict interior angles, not degenerate 0 or 180 degree cases, for its Regge closure program, a discrete approach to general relativity. The theorem removes the need to check arccos endpoint inputs in downstream calculus once normal independence is available. What the declaration does not claim is broader. It does not assert that any particular tetrahedron satisfies the triple product condition; that is a separate hypothesis about the specific geometric realization. It does not claim anything about the physical meaning of the framework's constants or about the nature of space itself. It is a purely geometric statement about vectors in three-dimensional Euclidean space, proved from the definition of linear independence and the algebraic properties of the cross product and dot product.

/-- Edge-local scalar triple product nonvanishing implies adjacent face-normal
independence. -/
theorem adjacentFaceNormalsIndependent_of_triple_ne_zero
    (T : RealizedTet) (e : Fin 6)
    (htriple :
      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 ≠ 0) :
    AdjacentFaceNormalsIndependent T e := by
  unfold AdjacentFaceNormalsIndependent adjacentFaceNormals faceNormal
  dsimp at htriple ⊢
  exact faceNormals_independent_of_triple_ne_zero 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 _ _ _

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

What this page does not claim

The theorem does not assert that any particular tetrahedron satisfies the nonzero triple product condition. The theorem says nothing about the physical interpretation of the framework's constants or the nature of space. The result is purely about vectors in three-dimensional Euclidean space, not about the framework's ledger or recognition events.

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: