Geometry Cayley Menger Polynomial Cm3 Const Sq

The constant-square case

The Cayley-Menger polynomial is a classical tool of Euclidean geometry: a single polynomial in the six squared edge lengths of a tetrahedron whose value equals 288 times the square of the tetrahedron's volume. For a genuine tetrahedron with edge lengths a, b, c, d, e, f, the relation is 288V² = CM₃(a), where V is the volume. The polynomial itself is a fixed degree-3 expression in those six squared lengths, and it vanishes exactly when the six lengths cannot form a Euclidean tetrahedron at all.

The declaration cm3_constSq concerns the special case where all six squared edge lengths are equal to a single number s. The theorem states that cm3(fun _ => s) = 4 * s^3. In plainer terms: when every edge of the tetrahedron has the same squared length s, the Cayley-Menger polynomial evaluates to 4 times s cubed. This is not a new geometric discovery; it is a direct algebraic consequence of the polynomial's definition and its known scaling behavior. The framework's machine-checked library of formal theorems proves this identity by first establishing that scaling all squared lengths by a factor s multiplies the whole polynomial by s³, then applying that scaling law to the unit regular tetrahedron, whose CM value is already known to be 4.

The proof is computationally explicit. The library first proves cm3_regular_unit, showing that the unit regular tetrahedron, with all squared lengths equal to 1, gives a CM value of 4. It then proves cm3_scaling, showing that multiplying every squared edge length by s scales the polynomial by s³. Combining these two facts yields the constant-square result. The library also proves that the polynomial is smooth, meaning it has derivatives of every order, which matters for later work involving Hessians and second-variation matrices in Regge calculus.

What this theorem does not claim is just as important. It does not assert that any set of six equal squared lengths actually forms a Euclidean tetrahedron; the polynomial can be positive, zero, or negative depending on the lengths, and only positive values correspond to realizable tetrahedra. It does not compute a volume directly, since the relation 288V² = CM₃ requires the lengths to satisfy the triangle inequalities and other realizability conditions. It does not generalize to higher dimensions, where the Cayley-Menger determinant takes a different polynomial form. The theorem is a precise algebraic identity about a specific polynomial, verified by the framework's proof checker, and nothing more.

The value of this result lies in what it enables. Because the constant-square case is simple and exactly known, it provides a test point for the framework's broader program: comparing the genuine Regge second-variation coefficient matrix, computed from Cayley-Menger derivatives, against the area of each triangular face. A clean closed form for the simplest symmetric case gives the program a concrete anchor to verify its derivative machinery against, before moving to general tetrahedra where the algebra is far more tangled.

/-- A trivial but useful corollary: the regular CM value at common
squared-length `s` equals `s³ · 4`. -/
theorem cm3_constSq (s : ℝ) : cm3 (fun _ => s) = 4 * s ^ 3 := by
  have h := cm3_scaling regularUnitSqEdges s
  have h1 : cm3 regularUnitSqEdges = 4 := cm3_regular_unit
  have h2 : (fun e : Fin 6 => s * regularUnitSqEdges e) = (fun _ : Fin 6 => s) := by
    funext e
    unfold regularUnitSqEdges
    ring
  have h3 : cm3 (fun _ : Fin 6 => s) = s ^ 3 * cm3 regularUnitSqEdges := by
    rw [← h2]; exact h
  rw [h3, h1]
  ring

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

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 theorem does not assert that equal squared edge lengths always form a realizable Euclidean tetrahedron. The theorem does not compute a volume directly, since the 288V² relation requires additional realizability conditions. The theorem does not extend the polynomial form to higher-dimensional simplices.

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: