Geometry Cayley Menger Polynomial

The volume polynomial

The Cayley-Menger polynomial is the classical formula that connects the six edge lengths of a tetrahedron to its volume. For a tetrahedron with vertices 0, 1, 2, and 3, write the squared lengths of the edges as α, β, γ, λ, μ, and ν. The polynomial is a degree-3 expression in these six variables. Its value equals 288 times the square of the volume for a genuine Euclidean tetrahedron, so the formula is 288V² = CM₃(a). This relation is the workhorse of metric geometry: it lets you compute a tetrahedron's volume from nothing but its edge lengths, and it detects whether a given set of six lengths can form a tetrahedron at all.

The formula was known in the nineteenth century, and it generalizes Heron's formula for the area of a triangle. In the same way that Heron's formula uses the three side lengths of a triangle to find its area, the Cayley-Menger polynomial uses the six edge lengths of a tetrahedron to find its volume. The polynomial is symmetric in a precise sense: it treats the four faces of the tetrahedron on equal footing. A standard check is the regular tetrahedron with all edges of length 1, which has volume √2/12; the polynomial gives 288V² = 4. Another check is the right-angle tetrahedron with three mutually perpendicular unit edges, volume 1/6; the polynomial gives 288V² = 8. These two test points confirm the formula against known volumes.

In Recognition Science, the framework's machine-checked library of formal theorems defines this polynomial explicitly and proves its essential properties. The library defines the polynomial cm3 as a function of six squared edge lengths, and it proves that the value on the unit regular tetrahedron is 4 and on the right-angle unit tetrahedron is 8. It also proves that the polynomial is smooth: it is infinitely differentiable with respect to the squared edge lengths, which means all derivatives, including the Hessian needed for second-variation calculations, exist. This smoothness is built directly from standard calculus combinators, not assumed as an extra condition.

The library further proves a scaling law. If all squared edge lengths are multiplied by a common factor s, the polynomial's value scales by s³. This matches the classical fact that volume scales as s^(3/2), so its square scales as s³. The scaling law is a sanity check that the polynomial behaves correctly under uniform resizing of the tetrahedron. As a corollary, a tetrahedron with all squared edge lengths equal to s has Cayley-Menger value 4s³. These results prepare the ground for the framework's deeper program: comparing the second-variation matrix of the Regge action, computed from Cayley-Menger derivatives, component by component against the areas of the tetrahedron's faces. The polynomial is the tool that makes that comparison possible.

/-- The explicit Cayley-Menger polynomial in the six squared edge lengths. -/
def cm3 (a : SqEdges) : ℝ :=
  2 * ( a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)
      + a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)
      + a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)
      - a 0 * a 1 * a 3
      - a 0 * a 2 * a 4
      - a 1 * a 2 * a 5
      - a 3 * a 4 * a 5 )

/-- The Cayley-Menger value of the unit regular tetrahedron is 4.
Classical: `V_unit_regular = √2 / 12`, so `288 V² = 288 / 72 = 4`. -/
theorem cm3_regular_unit : cm3 regularUnitSqEdges = 4 := by
  unfold cm3 regularUnitSqEdges
  norm_num

/-- The Cayley-Menger value of the right-angle unit tetrahedron is 8.
Classical: `V = 1/6`, so `288 V² = 288/36 = 8`. -/
theorem cm3_rightAngle_unit : cm3 rightAngleUnitSqEdges = 8 := by
  unfold cm3 rightAngleUnitSqEdges
  norm_num

/-- The Cayley-Menger polynomial is `Cⁿ` for any natural order `n`.
Built explicitly from `ContDiff.add`, `ContDiff.sub`, `ContDiff.mul`. -/
theorem cm3_contDiff (n : ℕ∞) : ContDiff ℝ n cm3 := by
  have h0 := contDiff_eval n 0
  have h1 := contDiff_eval n 1
  have h2 := contDiff_eval n 2
  have h3 := contDiff_eval n 3
  have h4 := contDiff_eval n 4
  have h5 := contDiff_eval n 5
  have hconst : ContDiff ℝ n (fun _ : SqEdges => (2 : ℝ)) := contDiff_const
  -- Build linear combinations.
  have s1 : ContDiff ℝ n (fun a : SqEdges => a 1 + a 2 + a 3 + a 4 - a 0 - a 5) :=
    ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add (ContDiff.add h1 h2) h3) h4) h0) h5
  have s2 : ContDiff ℝ n (fun a : SqEdges => a 0 + a 2 + a 3 + a 5 - a 1 - a 4) :=
    ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add (ContDiff.add h0 h2) h3) h5) h1) h4
  have s3 : ContDiff ℝ n (fun a : SqEdges => a 0 + a 1 + a 4 + a 5 - a 2 - a 3) :=
    ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add (ContDiff.add h0 h1) h4) h5) h2) h3
  -- Three "balanced" cubic terms.
  have c1 : ContDiff ℝ n (fun a : SqEdges =>
      a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)) :=
    ContDiff.mul (ContDiff.mul h0 h5) s1
  have c2 : ContDiff ℝ n (fun a : SqEdges =>
      a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)) :=
    ContDiff.mul (ContDiff.mul h1 h4) s2
  have c3 : ContDiff ℝ n (fun a : SqEdges =>
      a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)) :=
    ContDiff.mul (ContDiff.mul h2 h3) s3
  -- Four monomial cubic terms.
  have nA : ContDiff ℝ n (fun a : SqEdges => a 0 * a 1 * a 3) :=
    ContDiff.mul (ContDiff.mul h0 h1) h3
  have nB : ContDiff ℝ n (fun a : SqEdges => a 0 * a 2 * a 4) :=
    ContDiff.mul (ContDiff.mul h0 h2) h4
  have nC : ContDiff ℝ n (fun a : SqEdges => a 1 * a 2 * a 5) :=
    ContDiff.mul (ContDiff.mul h1 h2) h5
  have nD : ContDiff ℝ n (fun a : SqEdges => a 3 * a 4 * a 5) :=
    ContDiff.mul (ContDiff.mul h3 h4) h5
  have inner : ContDiff ℝ n (fun a : SqEdges =>
        a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)
      + a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)
      + a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)
      - a 0 * a 1 * a 3
      - a 0 * a 2 * a 4
      - a 1 * a 2 * a 5
      - a 3 * a 4 * a 5 ) :=
    ContDiff.sub (ContDiff.sub (ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add c1 c2) c3) nA) nB) nC) nD
  show ContDiff ℝ n cm3
  unfold cm3
  exact ContDiff.mul hconst inner

theorem cm3_scaling (a : SqEdges) (s : ℝ) :
    cm3 (fun e => s * a e) = s ^ 3 * cm3 a := by
  unfold cm3
  ring

What this page does not claim

The module does not prove the classical Cayley-Menger determinant formula from first principles; it defines the polynomial directly and verifies it on test points. The module does not establish any connection between the Cayley-Menger polynomial and the golden ratio or the forcing chain. The module does not prove that the second-variation matrix equals the face areas; it only prepares the polynomial for that comparison.

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/CayleyMengerPolynomial.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: