Geometry Gram Cayley Menger Cm3 Sq Edge Of Points Eq 8 Det Gram

The Gram-Cayley-Menger bridge

The Cayley-Menger determinant and the Gram determinant are two classical routes to the same geometric fact: the volume of a simplex. For a tetrahedron, the Cayley-Menger determinant is built purely from the six squared edge lengths, while the Gram determinant is built from the dot products of the three edge vectors meeting at one vertex. The declaration cm3_sqEdgeOfPoints_eq_8_det_gram proves, in the framework's machine-checked library of formal theorems, that for any realized tetrahedron the Cayley-Menger polynomial of its squared edge data equals eight times the determinant of its Gram matrix.

The statement is a pure algebraic identity. Given a symmetric 3 by 3 real matrix G, the squared edges it generates are the diagonal entries G 0 0, G 1 1, G 2 2 for the three edges from vertex 0, and the combinations G i i + G j j - 2 G i j for the opposite edges. The theorem then verifies, by expanding both determinants and simplifying with the symmetry condition, that the Cayley-Menger polynomial of those six numbers is exactly 8 times det G. No metric, no coordinates, and no distance formula enter the proof; it is a polynomial identity in the entries of G.

The bridge to actual geometry comes from a second theorem: for a realized tetrahedron in Euclidean space, the squared edge lengths extracted from the points agree with the squared edges generated from the Gram matrix of the three basepoint edge vectors. Composing the two results yields the main theorem, which states that for any realized tetrahedron, the Cayley-Menger polynomial of its squared edge data equals 8 times the determinant of its Gram matrix. From this, the framework derives the volume equivalence: the squared volume computed from Cayley-Menger data equals the squared volume computed from the Gram determinant, up to the same constant factor.

What the theorem does not claim is just as important. It does not assert that every symmetric 3 by 3 matrix corresponds to a realized tetrahedron; a Gram matrix must also be positive semidefinite to come from actual points. It does not compute any particular volume or compare the formula against measured data. It is a formal identity between two algebraic expressions, proved once for all symmetric matrices and then specialized to realized tetrahedra. The framework's library uses this bridge as a step toward relating two classical volume formulas, but the theorem itself is a statement about polynomials and determinants, not about physical space.

/-- For a realized tetrahedron, `cm3` of the extracted squared-edge data
equals `8 * det(Gram)`. -/
theorem cm3_sqEdgeOfPoints_eq_8_det_gram (T : RealizedTet) :
    cm3 (sqEdgeOfPoints T) = 8 * Matrix.det (gram3 T) := by
  rw [sqEdgeOfPoints_eq_sqEdgesFromGram]
  exact cm3_sqEdgesFromGram_eq_8_det (gram3 T) (gram3_symm T)

/-- 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)

/-- The realized tetrahedron satisfies the Gram/Cayley-Menger volume theorem. -/
theorem gram_cayley_menger_realized (T : RealizedTet) :
    volumeSqFromCM T = volumeSqFromGram T := by
  unfold volumeSqFromCM volumeSqFromGram
  rw [cm3_sqEdgeOfPoints_eq_8_det_gram]
  ring

What this page does not claim

The theorem does not assert that every symmetric 3 by 3 matrix corresponds to a realized tetrahedron. The theorem does not compute any particular volume or compare the formula against measured data. The theorem is a statement about polynomials and determinants, not about physical space.

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: