basisEdgeVector_linearIndependent
plain-language theorem explainer
The three edge vectors from a fixed base vertex of a realized tetrahedron to the other three vertices are linearly independent over ℝ. Tetrahedral and Regge-geometry arguments in the RS stack cite this as the bridge from vertex nondegeneracy to edge-frame freeness. The proof rewrites the tetrahedron's affine independence as linear independence of vsubs from the base vertex, then composes with a Fin-3 reindexing of the three non-base labels.
Claim. For every realized tetrahedron $T$, the three coordinate edge vectors from a fixed base vertex to the other three vertices are linearly independent over $\mathbb{R}$.
background
The module develops the strict dihedral-interior step for the Regge closure program. Its analytic core is that two linearly independent adjacent face normals have normalized dot product strictly in $(-1,1)$, so arccos endpoints can be dropped from downstream calculus once normal independence is known.
A realized tetrahedron carries four points in Euclidean 3-space together with a nondegeneracy hypothesis. That hypothesis is affine independence of the four vertices. Fixing base vertex $0$, the three vectors from that base to the remaining vertices are the natural edge frame; the theorem asserts this frame is free over $\mathbb{R}$.
Sibling results then lift edge-frame freeness to nonzero face normals and to independence of adjacent face normals (via a nonzero cross product), which is exactly the geometric reduction the module advertises.
proof idea
Start from $T$'s nondegeneracy field. Rewrite it via Mathlib's affineIndependent_iff_linearIndependent_vsub at base index $0$, obtaining linear independence of the three vsubs from vertex $0$ to the other three vertices, indexed by ${j:\mathrm{Fin},4\mid j\neq 0}$.
Build an explicit equivalence $e:\mathrm{Fin},3\simeq{j\mid j\neq 0}$ sending $0,1,2$ to $1,2,3$ (with the impossible $j=0$ case eliminated). Apply LinearIndependent.comp along $e$ using injectivity of $e$. Convert the resulting family to basisEdgeVector T by a pointwise fin_cases identity on the three indices.
why it matters
This is the first geometric reduction step in the module's chain from RealizedTet nondegeneracy to strict dihedral interior. Once the base edge frame is free, siblings obtain nonzero face normals and the criterion that adjacent face normals are independent iff their cross product is nonzero. That independence forces the normalized normal-normal dot product into $(-1,1)$, which is the strict-interior input Regge closure needs.
No downstream theorem currently records a hard edge into this declaration, but the module's stated purpose is precisely to keep this affine-to-edge independence target explicit while clearing arccos endpoint hypotheses from later calculus. In the broader RS geometry layer it is ordinary Euclidean 3-space bookkeeping (consistent with the forced $D=3$ landmark), not a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.