coordEdgeVector_dot_base_sub
plain-language theorem explainer
For a realized tetrahedron, the Euclidean dot product of any two coordinate edge vectors equals the same product after both edges are rewritten as differences of edges from vertex 0. Anyone building face normals or dihedral cosines from embedded tet coordinates would cite this. The proof is a two-rewrite application of the base-subtraction identity for each edge.
Claim. Let $T$ be a realized tetrahedron in $\mathbb{R}^3$ and let $a,b,c,d\in\{0,1,2,3\}$. Write $e_{ij}$ for the coordinate edge vector of $T$ from vertex $i$ to vertex $j$. Then $e_{ab}\cdot e_{cd}=(e_{0b}-e_{0a})\cdot(e_{0d}-e_{0c})$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products of edge vectors, then 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 from DihedralCayleyMenger.
A realized tetrahedron supplies four points in $\mathbb{R}^3$. The coordinate edge vector from $i$ to $j$ is the difference of those embedded vertices. The sibling identity coordEdgeVector_eq_base_sub states that every edge equals the difference of the two edges from a fixed base vertex $0$: $e_{ab}=e_{0b}-e_{0a}$. Rebasing at $0$ is the standard move before forming face normals as cross products in a common origin frame.
Dot products of such rebased edges feed the Gram data that appear in normal-normal inner products and in the numerator of the geometric dihedral cosine.
proof idea
One-line tactic proof: rewrite both sides of the claimed equality by applying the base-subtraction identity twice, once to each edge. After coordEdgeVector_eq_base_sub on $(a,b)$ and on $(c,d)$, the left-hand side is literally the right-hand side, so the goal closes by definitional equality of the rewritten terms. No inner-product algebra is needed beyond the rewrite.
why it matters
Sits in the geometric half of the Berger cofactor pipeline for tetrahedral dihedral angles. Face normals and the geometric dihedral cosine (siblings such as faceNormal, geometricDihedralNumerator, geometricDihedralCos) need edge vectors expressed relative to a common origin; this lemma packages the corresponding identity at the level of pairwise dots.
Module doc states the remaining goal: identify the geometric cosine with the Cayley-Menger cofactor ratio. This identity is pure Euclidean bookkeeping toward that match. No downstream consumers are wired yet (used_by empty), so it is infrastructure rather than a cited leaf. It does not itself touch RS forcing landmarks (T5-T8, RCL, phi); it is classical 3D tet geometry supporting later Recognition geometry claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.