faceNormal_edge1_right_self_gram
plain-language theorem explainer
Squared norm of the face normal on vertices (0,2,3) equals the 2×2 Gram determinant of the two edges from the apex that span that face. Used when converting geometric normal data into Gram entries inside the Berger/Cayley–Menger dihedral pipeline. Proof rewrites by the cross-product self-dot identity, then unfolds coordinate dots into gram3.
Claim. For a realized tetrahedron $T$, $\|N\|^2 = G_{11}G_{22}-G_{12}G_{21}$, where $N$ is the coordinate face normal on vertices $(0,2,3)$ and $G$ is the Gram matrix of the three edge vectors based at vertex $0$, with indices $1,2$ labeling edges $0\to 2$ and $0\to 3$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products, then the normalized inner product of adjacent face normals. The target is Berger's cofactor formula, matching that geometric cosine to a Cayley–Menger cofactor ratio.
A realized tetrahedron supplies four points in Euclidean 3-space. Edge vectors from vertex $0$ form a basis triple; their Gram matrix $G=\mathrm{gram3}$ records all pairwise inner products. The face normal on $(a,b,c)$ is the coordinate cross product of the two edges from $a$ along that face.
Upstream, faceNormal_dot_self reduces $|N|^2$ to the $2\times 2$ Gram determinant of those two edge vectors in coordinate form. Coordinate dots agree with the real Euclidean inner product of the corresponding edge vectors, so the identity lands in $G$.
proof idea
One short tactic proof. First rewrite with the general self-dot identity for face normals, which expands $|N_{023}|^2$ into the $2\times 2$ determinant of coordinate edge-vector dots on edges $0\to 2$ and $0\to 3$. Then simplify: replace each coordinate dot by the Euclidean inner product, unfold the Gram matrix and the basis-edge indexing (basis slots $1,2$ are exactly those two edges), and the right-hand side is $G_{11}G_{22}-G_{12}G_{21}$.
why it matters
Feeds the next lemma in-module: the Cayley–Menger $3\times 3$ cofactor on the matching diagonal equals $-4$ times this squared normal. That step is the bridge from pure geometry (cross-product normals) into the CM minor algebra used for dihedral cosines.
In the broader Recognition geometry stack, dihedral data on realized tets sit under the Freudenthal/two-cube scaffolding and the $D=3$ forcing (T8). Closing the Berger identification gives a fully algebraic route from edge-length Gram data to dihedral cosines without choosing an extrinsic frame beyond the apex basis.
No open scaffold here: the claim is proved and only specializes one face/index pattern needed by the cofactor comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.