faceNormal_edge3_left_self_gram
plain-language theorem explainer
The squared norm of the face normal on vertices (1,2,0) of a realized tetrahedron equals the 2×2 Gram determinant of the two edge vectors based at vertex 0 that span the complementary edges. Anyone matching geometric dihedral data to Cayley–Menger cofactors cites this identity. The proof expands the cross-product self-dot by the Lagrange identity, rebases both edges at vertex 0, and reduces to Gram entries by ring normalization.
Claim. For any realized tetrahedron $T$, let $n$ be the coordinate face normal of the face through vertices $1,2,0$. Then $\|n\|^2 = G_{00}G_{11}-G_{01}G_{10}$, where $G$ is the Gram matrix of the three edge vectors based at vertex $0$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals as cross products of coordinate edge vectors in $\mathbb{R}^3$, and the normalized inner product of two adjacent face normals. The target is Berger's cofactor formula, equating that geometric cosine to a Cayley–Menger cofactor ratio.
A realized tetrahedron supplies four points in Euclidean space and the associated edge vectors. The coordinate edge vector from $a$ to $b$ is the $\mathbb{R}^3$ representative of that edge; it may be rebased at vertex $0$ as a difference of base edges. The face normal through $(a,b,c)$ is the cross product of the two edges from $a$. Its squared self-dot expands by the Lagrange (cross-dot-cross) identity to a $2\times 2$ Gram determinant of those edges.
The Gram matrix gram3 records inner products of the three base edge vectors from vertex $0$. Upstream, coordinate dots agree with the real inner product of Euclidean edge vectors, so the algebraic Gram data match the geometric edge geometry.
proof idea
Start from the general self-dot identity for face normals: $|u\times v|^2=|u|^2|v|^2-(u\cdot v)^2$. Specialize to edges from vertex $1$ toward $2$ and $0$. Rebase both coordinate edges at vertex $0$ via the difference formula. Replace every coordinate dot by the corresponding real inner product of edge vectors, then unfold the Gram and basis-edge definitions. Convert self-inner-products to squared norms, expand the bilinear form of the two differences with the usual left/right subtraction rules and symmetry of the real inner product, and finish by ring normalization to the stated $2\times 2$ Gram determinant.
why it matters
This identity is the geometric half of the bridge from face-normal squared length to a Cayley–Menger $3\times 3$ cofactor. Downstream, the cofactor on the right diagonal of the squared-edge CM matrix equals $-4$ times this same normal squared norm; the proof of that comparison rewrites through the present lemma and the Gram form of squared edges.
Together those steps feed the module's remaining goal: Berger's cofactor formula, which identifies the geometric dihedral cosine (normalized inner product of adjacent face normals) with the CM cofactor ratio in the companion Cayley–Menger module. In the broader Recognition geometry stack this is pure Euclidean bookkeeping for tetrahedral angles, not a forcing-chain step, but it is required scaffolding for any later claim that dihedral data are forced by discrete edge lengths on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.