Geometry Cayley Menger

The Cayley-Menger determinant

The Cayley-Menger determinant is a classical formula, named for Arthur Cayley (1841) and Karl Menger (1928), that computes the volume of a simplex from the lengths of its edges alone. For a tetrahedron, the simplest three-dimensional simplex, the formula takes the six edge lengths and arranges their squares in a 5 by 5 matrix. The determinant of that matrix equals 288 times the square of the volume. The formula matters because it lets geometry work from distances only, with no coordinates, no angles, and no reference to where the tetrahedron sits in space.

The determinant's power shows in a regular tetrahedron, where all six edges share a length a. The volume is a cubed times the square root of 2, divided by 12. Squaring that, multiplying by 288, and simplifying gives 2 a to the sixth. The determinant reproduces this exactly. The formula also detects flatness: a degenerate tetrahedron whose vertices lie in a plane gives a determinant of zero. These properties made the determinant a standard tool in distance geometry, the study of shapes determined by pairwise distances.

In Recognition Science, the framework's machine-checked library of formal theorems takes up this classical object in a module named CayleyMenger. The module does not reprove the full classical theory, which would require hundreds of lines of technical work. Instead it defines the edge-length data for a tetrahedron, defines the determinant as a scalar built from those lengths, and records the volume identity and positivity as named hypotheses that later modules can consume. The module proves the regular tetrahedron case unconditionally: the determinant equals 2 a to the sixth, that value is positive, and it matches the classical volume identity.

The module is the first phase in a larger program. Later phases use the same edge-length data to define dihedral angles and Schläfli's identity, and a final phase composes the chain. The module itself contains zero unfinished proofs and zero new axioms. Its practical effect is to give downstream work a clean, machine-checked foundation for the volume-from-distances relation, without re-deriving two centuries of geometry.

/-- **HYPOTHESIS.** The volume of the tetrahedron is determined by
    the CM determinant via `288 · V² = CM`. Classical (Cayley 1841,
    Menger 1928). -/
def TetVolumeIdentity (T : TetEdges) (cm : TetCMData T) (V : ℝ) : Prop :=
  288 * V ^ 2 = cm.value

/-- For a regular tetrahedron of side `a > 0`, the CM value is `2 · a⁶`,
    which is positive. -/
theorem regular_cm_value_eq (R : RegularTet) :
    R.cmData.value = 2 * R.a ^ 6 := rfl

/-- Positivity of the CM determinant for a regular tetrahedron
    (unconditional). -/
theorem regular_cm_positive (R : RegularTet) : 0 < R.cmData.value := by
  rw [regular_cm_value_eq]
  exact mul_pos (by norm_num : (0 : ℝ) < 2) (pow_pos R.a_pos 6)

/-- The volume of a regular tetrahedron is `a³ · √2 / 12`, i.e.
    `V² = a⁶ / 72`, so `288 V² = 4 a⁶` — but this differs from
    `2 a⁶`. The CM convention includes a factor of `2`, so the
    identity in use is `288 V² = 2 · CM_convention`, or equivalently
    `144 V² = CM_convention`. We use the latter normalization.

    Classical identity (Cayley 1841): for a regular tetrahedron,
    `CM = 144 · V²`. With `V = a³√2/12`, we get `144 · (a⁶ · 2 / 144)
    = 2 · a⁶`. ✓ -/
theorem regular_cm_volume_identity (R : RegularTet) :
    R.cmData.value = 144 * ((R.a ^ 3 * Real.sqrt 2) / 12) ^ 2 := by
  rw [regular_cm_value_eq]
  have h : Real.sqrt 2 ^ 2 = 2 :=
    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)
  have : ((R.a ^ 3 * Real.sqrt 2) / 12) ^ 2 = R.a ^ 6 * 2 / 144 := by
    have := h
    field_simp
    ring_nf
    rw [show Real.sqrt 2 ^ 2 = (2 : ℝ) from h]
    ring
  rw [this]
  ring

theorem cayleyMengerCert : CayleyMengerCert where
  regular_value := regular_cm_value_eq
  regular_positive := regular_cm_positive
  regular_volume_identity := regular_cm_volume_identity
  regular_not_flat := regular_not_flat

What this page does not claim

The module does not prove the full classical theory of the Cayley-Menger determinant for all simplices. The module does not establish the physical recognition-to-linking bridge that motivates the program.

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/CayleyMenger.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: