faceNormals_independent_of_triple_ne_zero
plain-language theorem explainer
A nonzero scalar triple product of three vectors in R^3 forces the two face normals sharing the first edge to be linearly independent. Anyone reducing affine independence of a tetrahedron to adjacent face-normal independence cites this edge-local step. The proof shows the shared edge is nonzero, rewrites the normals' cross product as the triple product times that edge, and applies the cross-product criterion for independence.
Claim. Let $u,v,w\in\mathbb{R}^3$. If the scalar triple product $u\cdot(v\times w)\neq 0$, then $u\times v$ and $u\times w$ are linearly independent over $\mathbb{R}$.
background
This module supplies the strict-interior step for the Regge closure program: two linearly independent adjacent face normals have normalized dot product strictly in $(-1,1)$, so dihedral angles stay off the flat endpoints. The analytic core is free of tetrahedral bookkeeping; the remaining reduction is to obtain adjacent face-normal independence from the affine-independence data of a realized tetrahedron.
Face normals here are ordinary cross products of edge vectors in coordinates $\mathrm{Fin},3\to\mathbb{R}$. The scalar triple product $u\cdot(v\times w)$ is the signed volume of the parallelepiped they span; nonvanishing is the local nondegeneracy hypothesis.
Upstream, the shared-edge identity states that if two face normals share the edge vector $u$, then $(u\times v)\times(u\times w)=(u\cdot v\times w),u$. That algebraic core converts triple-product nonvanishing into a nonzero cross of the two normals.
proof idea
First rule out $u=0$: if the shared edge vanished, the triple product would be zero, contradicting the hypothesis. Next rewrite the cross of the two candidate normals by the shared-edge identity: $(u\times v)\times(u\times w)$ equals the triple product times $u$. The right-hand side is a nonzero scalar times a nonzero vector, hence nonzero. Finally apply the standard equivalence that two vectors in $\mathbb{R}^3$ are linearly independent iff their cross product is nonzero.
why it matters
The immediate parent is the edge-indexed statement that a nonvanishing triple product on a realized tetrahedron yields adjacent face-normal independence for that edge. That parent is the bridge from the affine-independence field of a realized tet to the strict dihedral-interior calculus the module advertises: once normals are independent, normalized dots lie strictly between $-1$ and $1$, and arccos endpoint inputs can be dropped downstream.
In the broader Recognition geometry stack this is pure Euclidean linear algebra supporting Regge-style closure, not a forcing-chain landmark (T5–T8). It closes the local algebraic gap between volume nondegeneracy and normal independence so later dihedral estimates run without endpoint scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.