coordEdgeVector
plain-language theorem explainer
Extracts the ordinary Euclidean edge vector from vertex a to vertex b of a realized tetrahedron as a map Fin 3 → ℝ. Downstream face-normal, dihedral-cosine, and affine-independence lemmas all cite it as the basic edge datum. The body is a one-line unwrap: subtract the two vertex positions and drop the Lp packaging.
Claim. Given a realized tetrahedron $T$ with vertices $p:\mathrm{Fin}\,4\to\mathbb{R}^3$ and indices $a,b\in\{0,1,2,3\}$, the coordinate edge vector is the ordinary difference $p_b-p_a$, viewed as a function $\mathrm{Fin}\,3\to\mathbb{R}$.
background
A realized tetrahedron (RealizedTet) is four points $p_0,\ldots,p_3$ in Euclidean 3-space together with an affine-independence hypothesis. Positions live in Mathlib's EuclideanSpace ℝ (Fin 3), so differences are Lp-vectors; this definition strips that packaging to a plain coordinate map.
The ambient module builds the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products, then the normalized inner product of adjacent face normals. That geometric cosine is the target of the Berger cofactor identification with the Cayley–Menger ratio from DihedralCayleyMenger.
Coordinate edge vectors are the raw ingredients for those normals and for every linear-independence check that keeps faces nondegenerate.
proof idea
Pure definition, no proof obligations. Body is (T.p b - T.p a).ofLp: subtract the two embedded vertex positions, then convert the Lp difference into a function Fin 3 → ℝ. No lemmas are applied.
why it matters
This is the shared edge datum for the whole dihedral-cofactor pipeline. In-module it feeds coordEdgeVector_eq_base_sub, coordEdgeVector_dot_eq_inner, and coordEdgeVector_dot_base_sub, which rewrite dots after rebasing at a fixed vertex. Downstream in AffineIndepInterior it appears in face-normal nonvanishing (faceNormal_ne_zero_of_edgeVectors_linearIndependent), adjacent-normal cross-product identities, triple-product independence, and the base-to-three-vertices linear-independence theorem that unpacks T.nondegenerate.
Those facts underwrite the geometric dihedral cosine and, ultimately, the Berger cofactor formula equating that cosine to the Cayley–Menger cofactor ratio. In the broader RS geometry stack this is ordinary Euclidean scaffolding for tetrahedral hinges (Regge-style), not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.