Geometry Cayley Menger Polynomial Cm3 Regular Unit

A checkable tetrahedron

The Cayley-Menger determinant is a classical tool of geometry: a single polynomial expression in the six squared edge lengths of a tetrahedron that determines its volume. For a genuine Euclidean tetrahedron, the relation is 288 times the square of the volume equals the polynomial. This is not a new claim; it is a standard result, and the Recognition Science framework's machine-checked library of formal theorems has now verified one small piece of it.

The specific theorem, named cm3_regular_unit, checks the case of the unit regular tetrahedron, where all six edges have length 1. The classical volume of this shape is √2/12, so 288 times the square of the volume equals 288 divided by 72, which is 4. The theorem confirms that the framework's explicit polynomial, called cm3, evaluates to exactly 4 when all six squared edge lengths are set to 1. The proof is a direct computation: it unfolds the definition and simplifies the arithmetic.

This is a consistency check, not a discovery. The framework defines its polynomial to match the classical one, and this theorem verifies that match on a single, highly symmetric test point. The same file also checks a right-angle unit tetrahedron, where three mutually perpendicular edges of length 1 meet at one vertex; there the polynomial evaluates to 8, matching the classical volume of 1/6. Both checks pass, which means the explicit polynomial agrees with the classical determinant on these two simple shapes.

The theorem also establishes that the polynomial is smooth: it is infinitely differentiable, a property that will matter for later derivative computations. And it shows the polynomial scales correctly: if all squared edge lengths are multiplied by a factor s, the polynomial's value multiplies by s³, matching the fact that volume scales as s^(3/2). These are structural properties of the polynomial itself, verified by the machine-checked library.

What this theorem does not claim is broader. It does not prove the Cayley-Menger formula for all tetrahedra; it checks only two specific cases. It does not say anything about the physical meaning of the polynomial, about recognition costs, or about why a tetrahedron matters in physics. It is a small, precise, and verified step in a larger program, and its value lies in being exactly that: a reliable brick, not a finished building.

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

It does not prove the Cayley-Menger formula for all tetrahedra, only for two test points. It does not connect the polynomial to any physical or recognition-theoretic concept. It does not establish that the polynomial is the only possible expression for volume.

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: