Geometry Cayley Menger Cayley Menger Cert

The Cayley-Menger certificate

The Cayley-Menger determinant is a classical tool from 1841, due to Arthur Cayley, that encodes the volume of a simplex from the lengths of its edges. For a tetrahedron, the object with four vertices and six edges, the determinant of a specific 5 by 5 matrix built from the squared edge lengths equals 288 times the square of the volume. Karl Menger's 1928 theorem states the converse: a set of edge lengths describes a genuine Euclidean tetrahedron exactly when this determinant is positive. The formula turns a question about geometry into a question about algebra.

For a regular tetrahedron, one where all six edges share the same length a, the volume is a³√2/12. Substituting this into the Cayley-Menger relation gives 144 times the squared volume, which simplifies to 2a⁶. The determinant therefore evaluates to 2a⁶ for a regular tetrahedron, a positive number that confirms the shape is not flat.

In Recognition Science, the machine-checked library of formal theorems records this classical content in a structure named CayleyMengerCert, a packaged certificate. The certificate bundles four statements about regular tetrahedra: the determinant equals 2a⁶, this value is positive, the volume identity holds through the formula 144V² = 2a⁶, and the shape is not flat. The declaration cayleyMengerCert proves all four statements hold, with zero gaps and zero new axioms.

The certificate deliberately stops at the regular case. The full Euclidean-geometry content for arbitrary tetrahedra, including positivity for all non-degenerate shapes and invariance under rigid motions, is classical and lives in the piecewise-flat geometry literature. In the library, those are long, technical proofs that would expand the module by several hundred lines without advancing the bridge theorem. The module instead records the general volume identity and positivity as named hypotheses, structures that downstream modules can consume, matching the pattern of recording the classical Cheeger-Müller-Schrader result as a hypothesis rather than reproving decades of geometry.

What the certificate changes is practical. Phase C2 can use the Cayley-Menger cosine formula to define dihedral angles, Phase C3 can use the same data for Schläfli's identity, and Phase C5 composes the whole chain. The regular tetrahedron now has a checked foundation, and the path to the broader bridge is open.

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

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

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

What this page does not claim

The certificate does not prove positivity of the Cayley-Menger determinant for all non-degenerate tetrahedra. The certificate does not establish invariance of the determinant under Euclidean motions. The certificate does not prove the general volume-formula equivalence for arbitrary simplices.

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: