coordEdgeVector_from_base_linearIndependent
plain-language theorem explainer
Coordinate edge vectors from any fixed base vertex of a realized tetrahedron to the other three vertices are linearly independent over ℝ, under any ordering of those three. Anyone reducing tetrahedral edge geometry to coordinate triples cites this. The proof rewrites nondegeneracy as affine independence of vertices, composes with the ordering equivalence, then transfers independence into coordinate space.
Claim. Let $T$ be a realized tetrahedron with four vertices in Euclidean space. Fix a base vertex $b$ and any bijection ordering the remaining three vertices. Then the three coordinate edge vectors from $b$ to those vertices are linearly independent over $\mathbb{R}$.
background
The module supplies the strict-interior step for the Regge closure program: two linearly independent adjacent face normals have normalized dot product strictly in $(-1,1)$. The geometric reduction is to obtain adjacent face-normal independence from the affine-independence field of a realized tetrahedron, so arccos endpoint inputs can be dropped downstream.
A realized tetrahedron carries four points that are affinely independent (nondegenerate). Affine independence at a base vertex is equivalent to linear independence of the three displacement vectors from that base to the other vertices. Coordinate edge vectors are the images of those displacements in the coordinate chart used by the geometry layer; the chart preserves linear independence of Euclidean edge triples.
The ordering of the three non-base vertices is an arbitrary equivalence $\mathrm{Fin},3\simeq{j:\mathrm{Fin},4\mid j\neq b}$, so the statement is basis-order free.
proof idea
Start from nondegeneracy of $T$. Rewrite it via the standard equivalence between affine independence of the four points and linear independence of the three Euclidean displacements from the chosen base. Compose that independent family with the given equivalence on the three non-base indices (using injectivity of the equivalence) to reindex without losing independence. Transfer the resulting Euclidean triple into coordinate space by the chart lemma that coordinate images of linearly independent Euclidean edge vectors remain linearly independent. The goal is exactly that coordinate family.
why it matters
This is the base-vertex form of edge-vector independence used to build edge-opposite coordinate triples. The sole recorded consumer is edge_opposite_coord_triple_linearIndependent: for each tetrahedral edge, the shared edge together with the two vectors to the opposite vertices form a linearly independent coordinate triple. That triple feeds face-normal constructions and the adjacent-normal independence criterion (cross product nonzero), which is the analytic core of the strict dihedral-interior step.
In the broader Recognition geometry stack this sits under the $D=3$ spatial forcing (T8) and the Regge-style discrete curvature bookkeeping that needs strict interior dihedral angles rather than boundary arccos values. It closes a bookkeeping gap: nondegeneracy of the tetrahedron alone yields ordered coordinate independence at every base, with no extra metric hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.