faceNormal
plain-language theorem explainer
The outward-style face normal of a tetrahedron face through vertices a,b,c is the ordinary cross product of the two edge vectors from a. Anyone working the Euclidean side of tetrahedral dihedral cosines cites it. The body is a one-line definition: cross of the two coordinate edge vectors.
Claim. For a realized tetrahedron $T$ in $\mathbb{R}^3$ and vertices $a,b,c\in\{0,1,2,3\}$, the face normal through $(a,b,c)$ is the coordinate vector $n_{abc}:=v_{ab}\times v_{ac}\in\mathbb{R}^3$, where $v_{ab}$ and $v_{ac}$ are the edge vectors of $T$ from $a$ to $b$ and from $a$ to $c$.
background
This module builds the Euclidean geometric side of the tetrahedral dihedral cosine: face normals from cross products, then the normalized inner product of two adjacent face normals. The target is Berger's cofactor formula, equating that geometric cosine with a Cayley-Menger cofactor ratio.
A realized tetrahedron supplies four points in $\mathbb{R}^3$. The coordinate edge vector from vertex $a$ to $b$ is the difference of those point coordinates. The face through $(a,b,c)$ is spanned by the pair of edges leaving $a$; its normal is their cross product in $\mathbb{R}^3$, valued as a map $\mathrm{Fin},3\to\mathbb{R}$.
No Recognition-cost or forcing-chain structure enters here: the object is pure Euclidean 3-geometry on a labeled 4-point set, preparatory to matching Gram/Cayley-Menger algebra.
proof idea
Pure definition, not a theorem. The body is the single term coordEdgeVector T a b ⨯₃ coordEdgeVector T a c: the Mathlib-style 3D cross product of the two edge vectors based at $a$. No lemmas are applied; downstream results unfold this abbreviation and invoke cross-product identities (cross-dot-cross, linear-independence criteria).
why it matters
This is the atomic geometric normal used throughout the dihedral pipeline. Downstream, adjacentFaceNormals packages the two face normals sharing a tetrahedral edge; nonvanishing and independence theorems (faceNormal_ne_zero_of_edgeVectors_linearIndependent, adjacentFaceNormalsIndependent_of_triple_ne_zero) and the shared-edge cross identity rest on it.
In the same module it feeds the diagonal cofactor identities that write Cayley-Menger 3-cofactors as $-4$ times squared normal norms (e.g. edge-0 left/right diagonal cofactors). Those equalities are the Euclidean half of Berger's formula, which will identify the geometric dihedral cosine with the cofactor ratio from DihedralCayleyMenger.
Framework role is local geometry supporting $D=3$ tetrahedral structure (T8), not a direct forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.