Geometry Gram Cayley Menger Cm3 Sq Edges From Gram Eq 8 Det

The Gram-Cayley-Menger bridge

The Cayley-Menger determinant is a classical formula that computes the volume of a simplex, such as a tetrahedron, from the squared lengths of its edges. The Gram determinant is another classical object, built from the dot products of vectors that span the tetrahedron from one vertex. For a tetrahedron in ordinary three-dimensional space, these two very different-looking computations must agree. The declaration cm3_sqEdgesFromGram_eq_8_det is a machine-checked proof of a precise algebraic identity: for any symmetric 3 by 3 matrix G, the Cayley-Menger polynomial of the squared edge data derived from G equals 8 times the determinant of G.

To see what this means, picture a tetrahedron with vertices 0, 1, 2, and 3. The matrix G holds the dot products of the three edge vectors from vertex 0. The squared edge lengths are then read off: the diagonal entries are the squared lengths of the three edges from vertex 0, and the off-diagonal entries combine through the formula |u - v|^2 = |u|^2 + |v|^2 - 2u·v to give the remaining three edges. The theorem states that feeding these six squared lengths into the Cayley-Menger polynomial produces exactly 8 times the determinant of G. This is a pure algebraic identity, true for any symmetric matrix, not just one that comes from actual points in space.

The theorem is proved in the framework's machine-checked library of formal theorems. The proof uses the symmetry of G to rewrite the determinant and then simplifies the polynomial with ordinary algebra. It does not rely on any geometric axioms or on the existence of a realized tetrahedron. The identity is a statement about matrices and polynomials. A separate theorem in the same module shows that for a realized tetrahedron, the squared edges extracted from actual points agree with the squared edges generated from the Gram matrix, and therefore the Cayley-Menger volume computation matches the Gram determinant computation.

What this declaration does not claim is just as important. It does not prove that any symmetric matrix corresponds to a realizable tetrahedron. A Gram matrix must also be positive semidefinite to come from actual vectors in space. The identity holds as algebra regardless. It also does not compute a volume directly; the Cayley-Menger polynomial is a step toward volume, and the factor 8 relates to the specific normalization used in the framework's definitions. The theorem is a bridge between two classical formulas, not a new geometric fact.

/-- Pure algebra: the tetrahedral Cayley-Menger polynomial generated by a
symmetric Gram matrix equals `8 * det G`. -/
theorem cm3_sqEdgesFromGram_eq_8_det (G : Matrix (Fin 3) (Fin 3) ℝ)
    (hsymm : ∀ i j, G i j = G j i) :
    cm3 (sqEdgesFromGram G) = 8 * Matrix.det G := by
  unfold sqEdgesFromGram cm3
  rw [Matrix.det_fin_three]
  have h10 : G 1 0 = G 0 1 := hsymm 1 0
  have h20 : G 2 0 = G 0 2 := hsymm 2 0
  have h21 : G 2 1 = G 1 2 := hsymm 2 1
  rw [h10, h20, h21]
  ring

/-- Pure algebra: the tetrahedral Cayley-Menger polynomial generated by a
symmetric Gram matrix equals `8 * det G`. -/
theorem cm3_sqEdgesFromGram_eq_8_det (G : Matrix (Fin 3) (Fin 3) ℝ)
    (hsymm : ∀ i j, G i j = G j i) :
    cm3 (sqEdgesFromGram G) = 8 * Matrix.det G := by
  unfold sqEdgesFromGram cm3
  rw [Matrix.det_fin_three]
  have h10 : G 1 0 = G 0 1 := hsymm 1 0
  have h20 : G 2 0 = G 0 2 := hsymm 2 0
  have h21 : G 2 1 = G 1 2 := hsymm 2 1
  rw [h10, h20, h21]
  ring

/-- The squared edges extracted from points agree with the squared edges
generated from the Gram matrix of the three basepoint edge vectors. -/
theorem sqEdgeOfPoints_eq_sqEdgesFromGram (T : RealizedTet) :
    sqEdgeOfPoints T = sqEdgesFromGram (gram3 T) := by
  funext e
  fin_cases e
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
    exact sqDist_eq_baseGram (T.p 0) (T.p 1) (T.p 2)
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
    exact sqDist_eq_baseGram (T.p 0) (T.p 1) (T.p 3)
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
    exact sqDist_eq_baseGram (T.p 0) (T.p 2) (T.p 3)

What this page does not claim

The identity does not imply that every symmetric matrix corresponds to a realizable tetrahedron. The theorem does not compute a volume directly; it establishes a polynomial identity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/GramCayleyMenger.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: