Geometry Gram Cayley Menger Sq Edge Of Points Eq Sq Edges From Gram

The bridge theorem

A tetrahedron has four vertices and six edges. The classical Cayley-Menger formula computes its volume squared directly from the six squared edge lengths. The Gram matrix approach instead starts with three edge vectors from one vertex, forms their 3 by 3 matrix of inner products, and derives the squared edge lengths from that matrix. The theorem sqEdgeOfPoints_eq_sqEdgesFromGram proves that these two routes always agree for a realized tetrahedron: the six squared edge lengths extracted from the actual points equal the six values generated from the Gram matrix of the three basepoint edge vectors.

The proof is pure algebra. The library defines sqEdgesFromGram to produce the six squared edge lengths: the three diagonal entries are the squared lengths of the three base vectors, and the three off-diagonal pairs use the identity that the squared distance between two points equals the sum of the squared base lengths minus twice their inner product. A separate theorem shows that the tetrahedral Cayley-Menger polynomial of these generated squared edges equals 8 times the determinant of the Gram matrix. Combining these two facts gives the main result: for any realized tetrahedron, the Cayley-Menger volume squared equals the Gram determinant volume squared, up to the same constant factor of 288 versus 36.

What the theorem does not claim is equally important. It does not assert that every symmetric 3 by 3 matrix corresponds to a realizable tetrahedron; that requires additional conditions on the matrix being positive semidefinite and satisfying triangle inequalities. It does not say anything about the volume itself, only about the squared volume. It also does not extend to higher dimensions, where the analogous statement involves larger matrices and different constants. The theorem is a bridge between two classical formulas in three-dimensional Euclidean geometry, not a claim about the framework's deeper structure.

In the Recognition Science framework, this bridge matters because it shows that two seemingly different descriptions of the same geometric object, one in terms of edge lengths and one in terms of inner products, carry exactly the same information. The framework models physical reality as a discrete record of events, and this theorem is part of its library of formal results about the geometry that such a record can support. The practical payoff is that any computation using one description can be translated into the other without loss, which is useful for checking consistency in geometric calculations.

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

/-- 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 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 realizable tetrahedron. The theorem does not say anything about the volume itself, only about the squared volume. The theorem does not extend to higher dimensions, where the analogous statement involves larger matrices and different constants.

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: