Geometry Cayley Menger Regular Cm Volume Identity

The volume identity

The Cayley-Menger determinant is a formula from 1841, due to Arthur Cayley and later generalized by Karl Menger in 1928, that computes the volume of a simplex from its edge lengths alone. For a tetrahedron, the simplest three-dimensional simplex, the determinant of a certain 5 by 5 matrix built from the six squared edge lengths gives 288 times the square of the volume. This is a classical result of Euclidean geometry, not a new discovery.

For a regular tetrahedron, all six edges have the same length a. The volume is a cubed times the square root of 2, divided by 12. Squaring this and multiplying by 288 gives 2 times a to the sixth power. The determinant itself, after expansion, also evaluates to 2 a^6, confirming the identity in this special case.

In Recognition Science, the machine-checked library of formal theorems records this classical identity as a theorem named regular_cm_volume_identity. The theorem states that for any regular tetrahedron with side length a, the Cayley-Menger value equals 144 times the square of the volume, which is the same statement with a different normalization. The library proves this by direct computation from the definitions, with no unproved assumptions. It also proves the value is positive and that a regular tetrahedron is not flat, meaning its volume is nonzero.

This theorem is a small but necessary step in a larger program. The library uses it as part of a chain to connect discrete geometry to general relativity, specifically to test a hypothesis about how curvature behaves in a simplicial approximation to spacetime. The volume identity is a building block; it does not by itself prove anything about gravity or about the physical universe.

What the theorem does not claim is important. It does not prove the general Cayley-Menger formula for arbitrary tetrahedra, which remains a classical result recorded as a hypothesis in the library. It does not establish that the determinant is positive for all non-degenerate tetrahedra, only for the regular case. And it does not connect the volume identity to any physical constant or to the Recognition Science framework's other results about the golden ratio or the fine-structure constant.

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

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

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

/-- A regular tetrahedron is non-flat. -/
theorem regular_not_flat (R : RegularTet) : ¬ IsFlat R.toTetEdges R.cmData := by
  unfold IsFlat
  rw [regular_cm_value_eq]
  have := regular_cm_positive R
  rw [regular_cm_value_eq] at this
  linarith

What this page does not claim

The theorem does not prove the general Cayley-Menger formula for arbitrary tetrahedra. The theorem does not establish positivity of the determinant for all non-degenerate tetrahedra. The theorem does not connect the volume identity to any physical constant or to other Recognition Science results.

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: