Geometry Cayley Menger Tet Cmdata

A scalar for tetrahedron volume

The Cayley-Menger determinant is a classical formula that encodes the volume of a simplex from its edge lengths. For a tetrahedron, the 5 by 5 matrix has zeros on the diagonal, ones in the first row and column, and squared edge lengths elsewhere; its determinant, up to a constant factor, equals the square of the volume. The formula is named after Arthur Cayley, who wrote it in 1841, and Karl Menger, who studied it in 1928. For a regular tetrahedron of side a, the determinant evaluates to 2 a^6, which matches 288 V^2 with V = a^3 sqrt(2)/12.

In Recognition Science, the machine-checked library of formal theorems records this classical content as a named structure, TetCMData, which is a scalar value defined from the six edge lengths. The library does not reprove the full Euclidean-geometry theorem that the determinant is positive for non-degenerate tetrahedra or that it is invariant under motion; those are long, technical proofs that the module deliberately leaves to the classical literature. Instead, the module defines the scalar, records the volume identity 288 V^2 = CM as a named hypothesis structure, and proves the degenerate cases unconditionally: a flat configuration has vanishing CM. The regular tetrahedron case is proved: for side a, the value is 2 a^6, which is positive, and the volume identity holds.

This minimal approach matches the pattern used elsewhere in the library, where classical results are recorded as named hypotheses rather than reproved from scratch. The module is Phase C1 of a larger program to discharge a hypothesis about Regge calculus; downstream modules use the CM cosine formula for dihedral angles and Schläfli's identity. The declaration establishes a clean interface: downstream code can consume the volume identity as a named hypothesis, without needing the full matrix-lifting machinery in the proof assistant.

What TetCMData does not claim is as important as what it does. It does not prove the classical theorem that the determinant is positive for all non-degenerate tetrahedra; that remains a named hypothesis. It does not prove the full Menger theorem about metric realization. It does not claim that the scalar is derived from the framework's cost function or forcing chain; it is a definitional choice, a scalar built from edge lengths, with the regular case proved. The module contains zero sorry and zero new axioms, but that audit means only that the proofs it does contain are machine-checked; it does not turn the named hypotheses into theorems.

/-- The Cayley-Menger determinant of a tetrahedron, *defined* by the
    explicit polynomial expansion. For a regular tetrahedron of side `a`,
    this evaluates to `2 · a⁶`, matching `288 · V² = 288 · (a³√2/12)² = 2a⁶`.

    The concrete closed form (5×5 CM determinant after expansion) is a
    6-degree polynomial in the squared edge lengths. We define it here
    as a hypothesis-supplied object, with the classical polynomial form
    recorded as a Prop. -/
structure TetCMData (T : TetEdges) where
  value : ℝ
  regular_tet_value :
    -- If all edges have the same length `a > 0`, the value is `2 · a⁶`.
    (∀ e, T.len e = T.len 0) → value = 2 * (T.len 0) ^ 6

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

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

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

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

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

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 determinant is not proved positive for all non-degenerate tetrahedra; positivity is a named hypothesis. The full Menger theorem on metric realization is not proved in this module. The scalar is not derived from the framework's cost function or 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: