volumeSqFromGram
plain-language theorem explainer
Squared Euclidean volume of a realized tetrahedron equals the determinant of its vertex-based edge Gram matrix divided by 36. Anyone bridging Gram and Cayley–Menger volume formulas cites this as the Gram-side definition. It is a one-line definitional wrapper of the classical Gram-volume identity, not a proved equality.
Claim. For a tetrahedron realized by four affinely independent points in Euclidean $3$-space, define the squared volume by $V^2 = \det(G)/36$, where $G$ is the $3\times 3$ Gram matrix of the three edge vectors based at one chosen vertex.
background
The module links abstract six squared-edge coordinates (Cayley–Menger layer) to actual points in Euclidean $3$-space. A realized tetrahedron is four points $p: \mathrm{Fin},4\to\mathbb{R}^3$ that are affinely independent; that nondegeneracy hypothesis is reserved for later strict dihedral-range and positive-volume arguments.
The Gram matrix $G$ is built from the three edge vectors based at vertex $0$: $G_{ij}=\langle e_i,e_j\rangle$. Its determinant is the squared volume of the parallelepiped they span. Classical solid geometry then recovers tetrahedron volume via $V=\sqrt{\det G}/6$, hence $V^2=\det G/36$.
This definition simply packages that classical identity on the realized-tetrahedron type so later theorems can compare it to the Cayley–Menger polynomial evaluated on extracted squared edges.
proof idea
Pure definition: evaluate the $3\times 3$ matrix determinant of the Gram matrix of the three basis edge vectors and divide by $36$. No lemmas are applied; the body is the classical formula written in Lean.
why it matters
This is the Gram-side half of the Gram–Cayley–Menger volume bridge for realized tetrahedra. Downstream, det_gram3_eq_36_volumeSq restates the same identity as an equality theorem, and GramCayleyMengerVolumeTheorem asserts that the Cayley–Menger volume squared equals this Gram volume for every realized tetrahedron. The realized and target-equivalence theorems in GramCayleyMenger discharge that bridge by rewriting through the Cayley–Menger determinant identity and a ring normalization.
In the broader Recognition geometry stack, the module sits between abstract edge data and Euclidean $3$-space embeddings (forced $D=3$ at T8). A clean Gram volume is needed before dihedral angles, Regge action, and rigidity statements can be stated on realized simplices rather than on formal edge sextuples alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.