Geometry Cayley Menger Regular Not Flat

A regular tetrahedron is not flat

A tetrahedron is the simplest three-dimensional solid: four triangular faces, four vertices, and six edges. When all six edges have the same positive length, it is a regular tetrahedron, the three-dimensional analogue of an equilateral triangle. The declaration regular_not_flat in the Recognition Science framework's machine-checked library of formal theorems establishes a basic geometric fact: such a solid is never flat.

Flatness here is defined through the Cayley-Menger determinant, a formula that encodes a simplex's volume from its edge lengths alone. For a tetrahedron with edge lengths L01 through L23, the determinant is a polynomial in the squared lengths; it vanishes exactly when the tetrahedron degenerates into a plane. The framework defines a flat configuration as one where this determinant equals zero. The theorem proves that for any regular tetrahedron with side length a greater than zero, the Cayley-Menger value is 2·a⁶, which is strictly positive, so the flatness condition cannot hold.

This result is unconditional: it requires no additional assumptions beyond the definition of a regular tetrahedron. The proof chains together two earlier results: the explicit evaluation of the determinant for equal edges, and the positivity of that value. The library also records the classical volume identity, 144·V² = CM, which for a regular tetrahedron with volume a³√2/12 gives the same positive value.

In Recognition Science, this theorem is a small but necessary step in a larger program. The framework models spacetime as a piecewise-flat simplicial complex, and the Cayley-Menger determinant is the tool that connects edge lengths to volumes and angles. Proving that regular simplices are non-flat is a prerequisite for later phases that define dihedral angles and verify the Schläfli identity. The declaration does not prove the full volume formula for arbitrary tetrahedra; that remains a named hypothesis, TetVolumeIdentity, recorded for downstream modules to consume.

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

/-- A degenerate "tetrahedron" where all four vertices coincide
    (all edges have length `a → 0`). This is a formal limit, not a
    valid `TetEdges` (edges must be positive). We state flatness
    via a `Prop` on the data. -/
def IsFlat (T : TetEdges) (cm : TetCMData T) : Prop :=
  cm.value = 0

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

What this page does not claim

The full volume formula for arbitrary tetrahedra is not proved; it is recorded as a named hypothesis. The theorem does not establish that all non-degenerate tetrahedra have positive Cayley-Menger determinant. The declaration does not connect the Cayley-Menger determinant to the Recognition Science 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: