edgeVector
plain-language theorem explainer
For a tetrahedron realized by four points in Euclidean 3-space, the edge vector from vertex i to j is the plain difference of position vectors. Anyone computing Gram matrices, face normals, or dihedral data from a realized tetrahedron cites this. The body is a one-line vector subtraction; no proof content.
Claim. Given a tetrahedron realized by four affinely independent points $p: \mathrm{Fin}\,4 \to \mathbb{R}^3$, the edge vector from vertex $i$ to vertex $j$ is the Euclidean vector $p_j - p_i \in \mathbb{R}^3$.
background
The module Euclidean Realizations of Tetrahedra bridges the abstract six squared-edge coordinates of the Cayley-Menger layer to concrete points in Euclidean 3-space. A realized tetrahedron packages a map $p$ from four vertex labels into $\mathbb{R}^3$ together with an affine-independence hypothesis, kept so that later volume and dihedral-range arguments stay strict.
Edge vectors are the elementary geometric atoms of that realization: once the four points are fixed, every subsequent Gram entry, face normal, and squared length is built from differences $p_j - p_i$. The ambient space is Mathlib's EuclideanSpace ℝ (Fin 3), so the usual real inner product is available immediately.
proof idea
Pure definition: return the difference of the two position vectors of the realized tetrahedron. No lemmas, no tactics; the body is T.p j - T.p i.
why it matters
This is the primitive used throughout the dihedral-cofactor layer. Downstream theorems equate coordinate edge-vector dots with the real inner product of these Euclidean edge vectors, and then expand face-normal self-Grams as $2\times 2$ minors of the three-edge Gram matrix built from basis edge vectors. Those identities feed the cofactor formula for dihedral cosines on a realized tetrahedron.
In the Recognition geometry stack the definition sits under the Euclidean realization of abstract edge data in $D=3$ (forcing step T8). It does not itself force dimension or regularity; it supplies the vector language in which volume-squared, Gram determinants, and dihedral ranges are later stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.