coordEdgeVector_eq_base_sub
plain-language theorem explainer
Any tetrahedral edge vector equals the difference of the two edge vectors from a fixed base vertex 0. Geometers working the Euclidean side of the Berger cofactor formula cite it to rewrite face-normal cross products in a common origin. The proof unfolds the coordinate definition and simplifies componentwise.
Claim. For a realized tetrahedron $T$ with vertices $p_0,p_1,p_2,p_3\in\mathbb{R}^3$ and any indices $a,b\in\{0,1,2,3\}$, the coordinate edge vector from $a$ to $b$ satisfies $p_b-p_a=(p_b-p_0)-(p_a-p_0)$.
background
The module builds the Euclidean geometric side of the tetrahedral dihedral cosine: face normals via cross products, then the normalized inner product of adjacent face normals. The target is the Berger cofactor formula equating that geometric cosine to a Cayley–Menger cofactor ratio.
A RealizedTet is four affinely independent points in Euclidean 3-space. The coordinate edge vector from vertex $a$ to $b$ is the $\mathbb{R}^3$ difference $p_b-p_a$ (as a function on Fin 3). Rebasing at vertex 0 means expressing every edge as a difference of two rays from $p_0$, which is the standard origin shift used before expanding Gram identities for face normals.
proof idea
Term-mode proof by definition chase. Unfold the coordinate edge vector to $p_b-p_a$ on both sides, then extend equality to each coordinate $k\in\mathrm{Fin},3$. Componentwise simplification of the vector identity $(p_b-p_a)_k=((p_b-p_0)-(p_a-p_0))_k$ finishes the argument; no external lemmas are required.
why it matters
This is the algebraic rebase step that lets every subsequent Gram expansion of face normals be written relative to a single origin. Downstream it is applied immediately in the dot-product rebase lemma, then repeatedly in the self-Gram identities for face normals on edges 3, 4, and 5 (left and right faces), and in the geometric dihedral numerator for edge 3.
Those identities feed the Euclidean cosine of adjacent face normals, which the module aims to match to the Cayley–Menger cofactor ratio (Berger formula). In the broader Recognition geometry stack this is scaffolding for dihedral angles on realized tetrahedra, not a forcing-chain landmark itself, but it is load-bearing for the geometric half of that identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.