coordEdgeVector_dot_eq_inner
plain-language theorem explainer
For any realized tetrahedron, the ordinary coordinate dot product of two edge vectors equals the Euclidean inner product of the same edges as elements of Euclidean 3-space. Anyone computing face-normal Gram entries or dihedral cosines from coordinate data cites this bridge. The proof unfolds both edge encodings and rewrites the inner product as a star-dot product, then simplifies.
Claim. Let $T$ be a tetrahedron realized by four affinely independent points in Euclidean $3$-space. For any vertex indices $a,b,c,d\in\{0,1,2,3\}$, the coordinate-wise dot product of the edge vectors from $a$ to $b$ and from $c$ to $d$ equals the real Euclidean inner product of those same edge vectors.
background
A RealizedTet is four points $p: \mathrm{Fin},4\to\mathbb{R}^3$ that are affinely independent. The Euclidean edge vector from vertex $i$ to $j$ is $p_j-p_i$ in EuclideanSpace. The coordinate edge vector is the same difference viewed as a plain map $\mathrm{Fin},3\to\mathbb{R}$ via the $\ell^2$ forgetful map ofLp.
This module builds the geometric side of the tetrahedral dihedral cosine: face normals from cross products of those edges, then the normalized inner product of adjacent face normals. The target is Berger's cofactor formula, equating that geometric cosine to a Cayley-Menger cofactor ratio.
The two edge encodings are definitionally the same displacement; only the ambient type differs (coordinate function versus Euclidean space). The theorem records that their natural bilinear forms agree.
proof idea
Term-mode proof in three steps. Unfold both coordEdgeVector and edgeVector so both sides are expressed from the same point differences. Rewrite the Euclidean-space inner product via EuclideanSpace.inner_eq_star_dotProduct, which identifies it with the star-dot product on coordinates. Finish with simp using commutativity of dotProduct to match the coordinate-side ⬝ᵥ notation.
why it matters
Face-normal self-Gram identities (faceNormal_edge*_left/right_self_gram and siblings) all reduce normal-squared lengths to $3\times 3$ Gram determinants of edge vectors. Each of those proofs rewrites through this lemma so that coordinate cross-product algebra lands on the Gram matrix built from Euclidean edges.
Those Gram identities feed faceNormal_dot_faceNormal and the geometric dihedral cosine (geometricDihedralCos), which the module aims to identify with the Cayley-Menger cofactor ratio (Berger). In the Recognition geometry stack this is the Euclidean half of the dihedral comparison used for tetrahedral packing and the $D=3$ forcing chain (T8), not a physics constant claim by itself.
Without the bridge, every normal-Gram calculation would have to re-prove the type-level identification of the two bilinear forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.