coord_linearIndependent_of_euclidean
plain-language theorem explainer
Coordinate extraction from Euclidean 3-space to plain coordinate triples preserves linear independence. Anyone reducing tetrahedron edge vectors or face normals to matrix rank cites this bridge. The proof pushes independence through the Mathlib linear equivalence EuclideanSpace.equiv and identifies the image with ofLp.
Claim. Let $v:\mathrm{Fin}\,3\to\mathbb{R}^3_{\mathrm{Euc}}$ be three vectors in Euclidean $3$-space. If $\{v_i\}$ is linearly independent over $\mathbb{R}$, then the coordinate triple obtained by forgetting the $L^2$ structure (the underlying maps $\mathrm{Fin}\,3\to\mathbb{R}$) is likewise 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)$. Downstream calculus then drops arccos endpoint inputs once normal independence is available.
EuclideanSpace $\mathbb{R}$ $(\mathrm{Fin}\,3)$ is Mathlib's $L^2$ product model of Euclidean $3$-space. The map ofLp (equivalently the linear equivalence EuclideanSpace.equiv) forgets the $L^2$ packaging and returns the underlying coordinate function $\mathrm{Fin},3\to\mathbb{R}$. Linear independence is a linear-algebraic property, so it is expected to be invariant under this equivalence; the theorem records that fact for the $3$-vector case used by tetrahedron bookkeeping.
Affine independence of the four vertices of a realized tetrahedron is rewritten, via the standard Mathlib identity, as linear independence of the three edge vectors from a fixed base. Those edge vectors live first in Euclidean space; this lemma moves them into plain coordinates.
proof idea
Let $L$ be the underlying linear map of the Mathlib equivalence EuclideanSpace.equiv : EuclideanSpace $\mathbb{R}$ $(\mathrm{Fin}\,3)\simeq(\mathrm{Fin}\,3\to\mathbb{R})$. Apply LinearIndependent.map'to the given independent family $v$, using that $L$ comes from a linear equivalence (so its kernel is trivial). The resulting independent family is $L\circ v$. A finalsimpaidentifies $L\circ v$ withfun i => (v i).ofLp`.
why it matters
Parent consumer is coordEdgeVector_from_base_linearIndependent: coordinate edge vectors from any fixed base vertex of a RealizedTet to the other three vertices are linearly independent for any ordering of those three. That theorem rewrites the tetrahedron's AffineIndependent field into coordinate linear independence, then needs exactly this bridge from Euclidean vectors to plain coordinates.
In the module's program, that independence feeds face-normal nonvanishing and adjacent-face-normal independence, which in turn give the strict dihedral-interior bounds required by Regge closure. The analytic core (normalized normal-dot in $(-1,1)$) is independent of tetrahedral bookkeeping; this lemma is the small linear-algebra hinge that lets the geometric reduction stay inside coordinates once the Euclidean structure has done its job. No forcing-chain landmark (T0–T8) is touched directly; the result is pure $3$D linear algebra in service of the geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.