Geometry Cayley Menger Derivatives

The derivative module

The Cayley-Menger polynomial is a classical object in geometry: a polynomial in the six squared edge lengths of a tetrahedron whose value is proportional to the square of the tetrahedron's volume. The formula goes back to the 19th century, when Karl Menger and Arthur Cayley showed that a set of distances between four points describes a real tetrahedron exactly when this polynomial takes the right sign. The polynomial vanishes when the four points lie flat, and its sign separates the configurations that fold into three dimensions from those that cannot exist as a rigid shape.

For a tetrahedron with vertices labeled 0 through 3, the six edges are indexed 0 through 5 in a fixed order: edge 0 connects vertices 0 and 1, edge 1 connects 0 and 2, and so on through edge 5 connecting 2 and 3. The central object is the polynomial CM₃, written as a sum of products of the squared edge lengths. The full expression is 2·[α·ν·(β+γ+λ+μ−α−ν) + β·μ·(α+γ+λ+ν−β−μ) + γ·λ·(α+β+μ+ν−γ−λ) − α·β·λ − α·γ·μ − β·γ·ν − λ·μ·ν], where the Greek letters stand for the six squared edge lengths in the indexed order.

The work proves a Taylor identity for this polynomial: if you add a small vector h to all six squared edge lengths at once, the value of CM₃ changes by a linear term, plus a quadratic term, plus a cubic term, with no higher-order remainder. The linear term is the gradient: six partial derivatives, each a quadratic polynomial in the six edge lengths. The quadratic term has a coefficient matrix, and the cubic term turns out to have zero coefficient along any single-edge perturbation. This means that if you change only one edge length, the volume squared changes exactly as a quadratic function of that change, with the linear coefficient given by the corresponding partial derivative and the quadratic coefficient by twice the diagonal Hessian entry.

The work writes each of the six partial derivatives in fully expanded form. For example, the derivative with respect to edge 0 is 2·(a₅·(a₁+a₂+a₃+a₄−a₀−a₅) − a₀·a₅ + a₁·a₄ + a₂·a₃ − a₁·a₃ − a₂·a₄). The other five follow the same pattern, each a quadratic polynomial in the six squared lengths. The work proves that these expressions are the true derivatives: each partial derivative function has the correct derivative at every point, and the full gradient map is the Fréchet derivative of CM₃.

In Recognition Science, the framework that derives physical structure from a forced cost function, this work feeds a larger program. The Regge second-variation matrix, which measures how the area of a triangle changes under edge-length variations, is built from these partial derivatives through the chain rule. The contribution is the explicit closed-form gradient: the exact polynomial expressions that let downstream computations avoid numerical differentiation and work with the true analytic derivatives. This is a piece of the framework's machinery for connecting the discrete geometry of triangulated surfaces to the continuous calculus of variations.

/-- **Polynomial Taylor identity** (algebraic):

`cm3 (a + h) = cm3 a + cm3_linear a h + cm3_quadratic a h + cm3_cubic h`. -/
theorem cm3_taylor (a h : SqEdges) :
    cm3 (fun i => a i + h i) =
      cm3 a + cm3_linear a h + cm3_quadratic a h + cm3_cubic h := by
  unfold cm3 cm3_linear cm3_partial0 cm3_partial1 cm3_partial2
         cm3_partial3 cm3_partial4 cm3_partial5
         cm3_quadratic cm3_cubic
  ring

/-- Partial derivative of `cm3` with respect to `a 0` (= α = squared edge (0,1)). -/
def cm3_partial0 (a : SqEdges) : ℝ :=
  2 * ( a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5) - a 0 * a 5
      + a 1 * a 4 + a 2 * a 3
      - a 1 * a 3 - a 2 * a 4 )

/-- Partial derivative of `cm3` with respect to `a 1` (= β = squared edge (0,2)). -/
def cm3_partial1 (a : SqEdges) : ℝ :=
  2 * ( a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4) - a 1 * a 4
      + a 0 * a 5 + a 2 * a 3
      - a 0 * a 3 - a 2 * a 5 )

/-- Partial derivative of `cm3` with respect to `a 2` (= γ = squared edge (0,3)). -/
def cm3_partial2 (a : SqEdges) : ℝ :=
  2 * ( a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3) - a 2 * a 3
      + a 0 * a 5 + a 1 * a 4
      - a 0 * a 4 - a 1 * a 5 )

/-- Partial derivative of `cm3` with respect to `a 3` (= λ = squared edge (1,2)). -/
def cm3_partial3 (a : SqEdges) : ℝ :=
  2 * ( a 2 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3) - a 2 * a 3
      + a 0 * a 5 + a 1 * a 4
      - a 0 * a 1 - a 4 * a 5 )

/-- Partial derivative of `cm3` with respect to `a 4` (= μ = squared edge (1,3)). -/
def cm3_partial4 (a : SqEdges) : ℝ :=
  2 * ( a 1 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4) - a 1 * a 4
      + a 0 * a 5 + a 2 * a 3
      - a 0 * a 2 - a 3 * a 5 )

/-- Partial derivative of `cm3` with respect to `a 5` (= ν = squared edge (2,3)). -/
def cm3_partial5 (a : SqEdges) : ℝ :=
  2 * ( a 0 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5) - a 0 * a 5
      + a 1 * a 4 + a 2 * a 3
      - a 1 * a 2 - a 3 * a 4 )

/-- The one-coordinate update polynomial, rewritten in Hessian form. -/
theorem cm3_update_hessianForm (a : SqEdges) (i : Fin 6) (t : ℝ) :
    cm3 (Function.update a i (a i + t)) =
      cm3 a + cm3_grad a i * t + (cm3_hessianDiag a i / 2) * t ^ 2 := by
  rw [cm3_update_polyform]
  unfold cm3_hessianDiag cm3_cubic_coeff
  ring

/-- `cm3GradientCLM` really is the Fréchet derivative of `cm3`. -/
theorem hasFDerivAt_cm3 (a : SqEdges) :
    HasFDerivAt cm3 (cm3GradientCLM a) a := by
  unfold cm3GradientCLM
  exact ((cm3_contDiff 1).differentiable_one a).hasFDerivAt

What this page does not claim

This work does not prove that the Cayley-Menger polynomial itself is derived from the framework's cost function. The work does not establish any physical law; it only provides the analytic machinery of derivatives. The connection from these derivatives to the Regge matrix or to spatial dimensions is not proved in this work.

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