adjacentFaceOppositeVertices
plain-language theorem explainer
Lookup table that, for each of the six edges of a labeled tetrahedron, returns the two opposite vertices of the faces meeting at that edge. Anyone computing dihedral angles, face normals, or Cayley–Menger cofactors on a realized tet cites it. The body is a pure pattern match on Fin 6 with no proof obligation.
Claim. A map $e \mapsto (u,v)$ from the six edges of a tetrahedron (indexed by $\mathrm{Fin}\,6$) to pairs of vertices in $\mathrm{Fin}\,4$, where $u$ and $v$ are the two vertices opposite the shared edge on the two adjacent faces. Explicitly: edge $0\mapsto(2,3)$, $1\mapsto(1,3)$, $2\mapsto(1,2)$, $3\mapsto(0,3)$, $4\mapsto(0,2)$, $5\mapsto(0,1)$.
background
A tetrahedron has four vertices and six edges. Each edge is the intersection of exactly two triangular faces; the third vertex of each of those faces is opposite the edge on that face. This definition packages that combinatorial fact as a total function on edge indices.
The ambient module builds the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products, then the normalized inner product of the two normals adjacent to a given edge. The target identity is Berger's cofactor formula, equating that geometric cosine to a ratio of Cayley–Menger cofactors.
Sibling helpers in the same file (coordinate edge vectors, face normals, geometric numerator and denominator square) all consume this opposite-vertex pair once an edge is fixed.
proof idea
No proof. The declaration is a definition by exhaustive pattern match on Fin 6, returning a hard-coded pair of opposite vertex indices for each edge label. There are no tactics, lemmas, or obligations.
why it matters
Every edge-local geometric construction in the dihedral pipeline begins here. Downstream, adjacentFaceNormals builds the two face normals from the shared edge and these opposite vertices; independence and cross-product identities (adjacentFaceNormals_cross_eq_triple_smul_edge, adjacentFaceNormalsIndependent_of_triple_ne_zero, edge_opposite_coord_triple_linearIndependent) quote the same pair. Inside this module the four edgewise theorems equating products of Cayley–Menger diagonal cofactors to sixteen times the geometric denominator square all route through the normals that this table selects. Without a fixed opposite-vertex convention the Berger cofactor identification cannot even be stated edge-by-edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.