basisEdgeVector
plain-language theorem explainer
Packs the three outgoing edge vectors from a fixed vertex of a realized Euclidean tetrahedron into a Fin-3-indexed family. Geometry and Regge-calculus developments cite it whenever Gram matrices, volumes, face normals, or affine independence are reduced to base edges. Pure definition by cases on the three edges leaving vertex 0.
Claim. Given a tetrahedron realized by four affinely independent points $p_0,p_1,p_2,p_3\in\mathbb{R}^3$, the basis edge map is the $\mathrm{Fin}\,3$-indexed family $0\mapsto p_1-p_0$, $1\mapsto p_2-p_0$, $2\mapsto p_3-p_0$.
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 is a map $p:\mathrm{Fin},4\to\mathbb{R}^3$ together with the hypothesis that the four points are affinely independent; that hypothesis later feeds strict dihedral range and positive-volume arguments.
The edge vector from vertex $i$ to $j$ is the ordinary difference $p_j-p_i$ in the ambient Euclidean space. The present definition simply selects the three edges that leave a distinguished base vertex (index 0) and packages them as a single $\mathrm{Fin},3$-indexed family. That packaging is the standard linear-algebraic input to the $3\times 3$ Gram matrix of the tetrahedron and to the linear-independence form of affine independence.
proof idea
Definition by exhaustive pattern match on $\mathrm{Fin},3$. Case 0 returns the edge vector from vertex 0 to 1; case 1 from 0 to 2; case 2 from 0 to 3. Each arm is a direct call to the sibling edge-vector difference. No lemmas or tactics are involved.
why it matters
This packing is the common substrate for the local Euclidean geometry of tetrahedra in the Recognition stack. Downstream, the three base edges are proved linearly independent from the affine-independence field of the realization, which is the bridge from combinatorial nondegeneracy to positive volume. The same family is the input to the $3\times 3$ Gram matrix whose determinant recovers $36$ times the squared volume, and it appears throughout the dihedral cofactor formulae that express squared face-normal lengths as $2\times 2$ Gram minors.
Those identities feed the rigorous Regge foundation and hinge-aware zero-mode analysis. In the broader forcing chain the ambient dimension is already fixed at $D=3$ (T8), so a three-vector basis at each tetrahedron is the natural local frame. The definition itself closes no open question; it is the shared coordinate convention that keeps volume, dihedral, and independence proofs aligned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.