Geometry Gram Cayley Menger Gram Cayley Menger Det Target Equiv

Two formulas, one volume

In Euclidean geometry, the volume of a tetrahedron can be computed from its six edge lengths using the Cayley-Menger determinant, a formula known since the nineteenth century. A second route starts with a Gram matrix, the table of dot products of three edge vectors meeting at one vertex. The classical fact that both routes give the same squared volume is what the framework's machine-checked library of formal theorems proves for realized tetrahedra.

The proof works by pure algebra. From a symmetric 3 by 3 Gram matrix G, the library defines six squared edge lengths: the three diagonal entries and three differences of diagonals minus twice the off-diagonals. Substituting these into the Cayley-Menger polynomial cm3 gives exactly 8 times the determinant of G. Since a realized tetrahedron's squared edges arise from its Gram matrix this way, the polynomial-level identity cm3 / 288 = det(G) / 36 follows for every realized tetrahedron.

The declaration gram_cayley_menger_det_target_equiv states that this determinant-level target is equivalent to the polynomial-level target. Both assert the same volume-squared equality, volumeSqFromCM T = volumeSqFromGram T, for every realized tetrahedron T. The equivalence is a definitional unfolding: cmDet3 equals cm3, so the two statements are the same proposition in different notation.

In Recognition Science, this bridge matters because it connects two ledger-style descriptions of the same geometric object. The framework models a tetrahedron through its squared-edge data, a discrete record of six numbers, and through its Gram matrix, another six numbers. The theorem shows these two records cannot disagree about volume. It is a proved result, not a hypothesis, and it holds for any realized tetrahedron in three-dimensional Euclidean space.

What the declaration does not claim is broader. It does not say the Cayley-Menger formula is valid for degenerate or higher-dimensional simplices, nor that any six numbers form a tetrahedron. It assumes a realized tetrahedron, meaning points in Euclidean space with the usual metric. The equivalence is about the two volume formulas, not about when a set of edge lengths can be realized geometrically.

/-- 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 determinant-level and polynomial-level targets are equivalent
because `cmDet3 = cm3`. -/
theorem gram_cayley_menger_det_target_equiv :
    GramCayleyMengerDetTheorem ↔ GramCayleyMengerTheorem := by
  constructor
  · intro h T
    have hT := h T
    rw [cmDet3_eq_cm3] at hT
    exact hT
  · intro h T
    have hT := h T
    rw [cmDet3_eq_cm3]
    exact hT

What this page does not claim

The theorem does not cover degenerate tetrahedra or simplices of dimension other than three. It does not state which six numbers can be realized as edge lengths of a tetrahedron. It makes no claim about the physical recognition-to-linking bridge that motivates the framework.

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: