Geometry Gram Cayley Menger Sq Dist Eq Base Gram

The basepoint identity

The law of cosines says that in any triangle, the square of one side equals the sum of the squares of the other two sides minus twice their product times the cosine of the included angle. The declaration sqDist_eq_baseGram proves the vector form of that same fact: for three points x, y, and z in ordinary three-dimensional space, the squared distance between y and z equals the squared distance from x to y plus the squared distance from x to z minus twice the dot product of the two vectors that leave x. The proof is pure algebra, expanding the squared norms and simplifying with the distributive and commutative properties of the inner product.

The identity matters because it lets a tetrahedron be described entirely by a 3 by 3 matrix of inner products, called the Gram matrix, a table of dot products among the three edge vectors that share a common vertex. From that matrix alone, the squared lengths of all six edges follow: the three diagonal entries are the squared lengths of the three edges from the base vertex, and each of the three remaining entries is built from two diagonal entries and one off-diagonal entry using exactly the basepoint identity. The library proves that this extraction agrees with the direct squared distances between the points, so the matrix carries the full shape information.

The same library then connects this Gram matrix picture to the classical Cayley-Menger determinant, a polynomial in the six squared edge lengths whose value determines the volume of a tetrahedron. The central theorem states that for any realized tetrahedron, the Cayley-Menger polynomial of its edge data equals eight times the determinant of its Gram matrix. Dividing by the appropriate constants shows that the two volume formulas, one from edge lengths and one from the Gram matrix, always agree. This is the bridge that lets a recognition framework treat a tetrahedron as a record of pairwise squared distances rather than a list of coordinates.

In Recognition Science, the framework models a discrete record of events, called a ledger, and this theorem is part of showing how geometric objects can be encoded by such records. The declaration does not claim that every symmetric matrix is a valid Gram matrix for real points; a matrix must be positive semidefinite to come from actual dot products. It also does not claim anything about tetrahedra in higher dimensions, where the 3 by 3 structure and the factor of eight no longer apply. The theorem is a local algebraic fact about three points in three-dimensional space, not a statement about the physical origin of space itself.

/-- Squared-distance identity induced by a basepoint Gram matrix. -/
private theorem sqDist_eq_baseGram
    (x y z : EuclideanSpace ℝ (Fin 3)) :
    ‖z - y‖ ^ 2 =
      ‖y - x‖ ^ 2 + ‖z - x‖ ^ 2 - 2 * inner ℝ (y - x) (z - x) := by
  rw [norm_sub_sq_real z y, norm_sub_sq_real y x, norm_sub_sq_real z x]
  simp [inner_sub_left, inner_sub_right, real_inner_comm]
  ring_nf

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

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

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

Not every symmetric 3 by 3 matrix is a valid Gram matrix; the theorem assumes the matrix comes from real points or is symmetric, not that it is positive semidefinite. The identity and the volume equivalence are stated for three-dimensional tetrahedra only, not for higher-dimensional simplices. The theorem does not address the physical origin of three-dimensional space or any recognition-theoretic derivation of dimension.

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: