Geometry Cayley Menger Regular Cm Positive

The regular tetrahedron's positive volume

The Cayley-Menger determinant is a formula that encodes the volume of a simplex, the generalization of a triangle to higher dimensions, using only its edge lengths. For a tetrahedron, the 3-dimensional simplex with four vertices and six edges, the determinant is a polynomial in the squared edge lengths. The classical identity, due to Cayley in 1841 and Menger in 1928, states that 288 times the square of the volume equals this determinant.

For a regular tetrahedron, where all six edges have the same length a, the determinant simplifies dramatically. The machine-checked library of formal theorems proves that the Cayley-Menger value equals 2·a⁶. Since a is positive, this value is strictly greater than zero. The theorem regular_cm_positive establishes this positivity unconditionally: no hypothesis about the shape being non-degenerate is needed, because regularity already guarantees it.

The positivity has a direct geometric meaning. A tetrahedron with a positive Cayley-Menger determinant is one that can be realized in Euclidean space with a non-zero volume. The theorem confirms that a regular tetrahedron is not flat; it does not collapse into a plane. This is also verified by the companion result that the regular tetrahedron is not flat, meaning its Cayley-Menger value is not zero.

The library also records the volume identity for the regular case: the Cayley-Menger value equals 144 times the square of the volume, where the volume is a³√2/12. This matches the classical formula and confirms the determinant's role as a volume certificate. The result is part of a larger program to discharge a hypothesis about Regge calculus, but the positivity theorem itself stands on its own as a statement about Euclidean geometry.

What the theorem does not claim is broader. It does not prove that the Cayley-Menger determinant is positive for every non-degenerate tetrahedron; that remains a named hypothesis, not a proved theorem. It also does not establish the full volume identity for arbitrary tetrahedra, which would require the classical Menger theorem. The library explicitly records these as hypotheses to be consumed by downstream modules, not as results it has derived.

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

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

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

What this page does not claim

The theorem does not prove positivity for all non-degenerate tetrahedra, which remains a named hypothesis. The theorem does not establish the full volume identity for arbitrary tetrahedra, which requires the classical Menger theorem. The theorem does not relate the Cayley-Menger determinant to the recognition science framework's forcing chain.

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: