faceNormal_edge0_right_self_gram
plain-language theorem explainer
Squared length of the face normal on vertices (0,1,3) of a realized tetrahedron equals the 2×2 Gram determinant G00 G22 − G02 G20. Cited when matching Euclidean face-normal geometry to Cayley–Menger cofactors along edge 0. Proof rewrites by the general normal self-dot identity, then simplifies edge inner products to Gram entries.
Claim. For a realized tetrahedron $T$, if $n$ is the Euclidean face normal built from the edge vectors spanning the face on vertices $(0,1,3)$, then $\|n\|^2 = G_{00}G_{22}-G_{02}G_{20}$, where $G$ is the $3\times 3$ edge Gram matrix of $T$.
background
This module supplies the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products of edge vectors, and the normalized inner product of the two normals adjacent to a shared edge. The target is the Berger cofactor formula, equating that geometric cosine to a Cayley–Menger cofactor ratio.
A realized tetrahedron carries four points in Euclidean space and the associated edge Gram data gram3. The face normal on an ordered triple of vertex indices is the cross product of two coordinate edge vectors from a common apex. Its squared length is therefore the Gram determinant of those two edge vectors.
The identity coordEdgeVector_dot_eq_inner identifies coordinate edge-vector dots with the corresponding Gram entries, so normal-square computations reduce to 2×2 minors of gram3.
proof idea
Short tactic proof. Rewrite the left-hand side by the general identity that the self-dot of a face normal equals the Gram determinant of its two generating edge vectors. Then simp with coordEdgeVector_dot_eq_inner, the definition of gram3, and the edge-vector constructors expands those dots into the explicit entries $G_{00}$, $G_{22}$, $G_{02}$, $G_{20}$ for the edge-0 right-adjacent face (indices 0 and 2).
why it matters
Closes the Gram evaluation of one adjacent normal square on edge 0. The sole downstream consumer is cmCofactor3_edge0_left_diag_eq_neg_four_normalSq, which rewrites the Cayley–Menger 3-cofactor on the diagonal as $-4$ times this normal square (after transporting squared edge lengths through the Gram–Cayley–Menger bridge).
That cofactor identity is a direct step toward the module’s Berger formula: geometric dihedral cosine (normalized normal inner product) equals the CM cofactor ratio. In the broader Recognition geometry stack this is pure Euclidean bookkeeping supporting rigid tetrahedral angle data, not a forcing-chain landmark (T5–T8), but it is required scaffolding for any later claim that ties discrete recognition geometry to classical dihedral measures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.