Pith. sign in
module module high

IndisputableMonolith.Geometry.GramCayleyMenger

show as:
view Lean formalization →

Links a symmetric 3×3 Gram matrix of edge vectors from one tetrahedron vertex to the six squared edge lengths that feed the Cayley-Menger layer. Anyone deriving volume or dihedral formulas from Gram data would cite it. Core identity: the cubic Cayley-Menger polynomial on those edges equals eight times det(G), then lifted to Euclidean realizations in R^3.

claimLet $G$ be a symmetric $3\times 3$ Gram matrix of edge vectors $(u,v,w)$ from a fixed vertex. The six squared edge lengths $e^2$ generated by $G$ satisfy $\mathrm{CM}_3(e^2)=8\det G$. The same identity holds for any Euclidean realization of those edges as points in $\mathbb{R}^3$.

background

Recognition Science geometry works with abstract six-tuples of squared edge lengths and with the cubic Cayley-Menger polynomial $\mathrm{CM}_3$ that encodes tetrahedron volume. The Cayley-Menger matrix module connects that polynomial to the classical $5\times 5$ bordered determinant and its cofactors. Separately, the realization module embeds those six squared lengths as actual points in Euclidean 3-space.

This module sits between those two layers. It starts from a Gram matrix $G=(\langle e_i,e_j\rangle)$ of the three edge vectors leaving vertex 0, builds the six squared lengths (three edge norms and three opposite-edge combinations via polarization), and compares $\mathrm{CM}_3$ on that data to $\det G$. The Gram picture is the natural algebraic source of a positive-semidefinite edge configuration before any ambient embedding is chosen.

proof idea

Definitions first: squared edges from a Gram matrix, then comparison maps between Gram-generated edges and edges of realized point sets. Algebraic core is an identity equating $\mathrm{CM}_3$ on Gram edges to $8\det G$, proved by expanding both sides as polynomials in the Gram entries. Realization lemmas show that squared distances among four points with a chosen base vertex recover exactly those Gram edges, so the determinant identity transfers to realized tetrahedra. Equivalence wrappers package the statement in the target form expected by the dihedral cofactor layer (both the polynomial form and a pure-determinant variant).

why it matters in Recognition Science

Feeds the dihedral cofactor module, whose doc-comment states it will identify the geometric cosine of a tetrahedral dihedral (normalized inner product of face normals) with a Cayley-Menger cofactor. That identification is the Berger cofactor formula target. Without the Gram-to-CM bridge, the cofactor side has no matched Euclidean Gram source.

In the broader RS geometry stack this is infrastructure for rigid tetrahedral combinatorics underlying eight-tick and $D=3$ forcing (T7, T8): volume and dihedral data must be expressible both from edge lengths and from a rank-at-most-3 Gram matrix. Parent consumer is DihedralCofactorFormula; upstream suppliers are CayleyMengerMatrix and TetrahedronRealization.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)