Geometry Cayley Menger Derivatives Cm3 Quadratic Single Perturb

A single-edge perturbation

The Cayley-Menger determinant is the classical object that answers a simple geometric question: given six lengths, can they be the edges of a tetrahedron in ordinary three-dimensional space? For a triangle, the analogous test is the familiar rule that any two sides must sum to more than the third. For a tetrahedron, the condition is that a certain polynomial in the six squared edge lengths, called CM₃, must be positive. This polynomial also appears in distance geometry, where it decides whether a set of pairwise distances can be embedded in Euclidean space.

The theorem cm3_quadratic_singlePerturb concerns what happens to CM₃ when you change exactly one of the six squared edge lengths, leaving the other five fixed. The change is described by a perturbation vector that is zero in every coordinate except one. The result is a clean formula: the quadratic part of the change in CM₃ equals a coefficient, which depends on the other five lengths, multiplied by the square of the perturbation size. In symbols, if you alter edge i by an amount t, the quadratic contribution is c_i(a) · t², where c_i(a) is a specific linear expression in the other lengths.

This is a machine-checked theorem in the framework's library of formal mathematics. It is not a new physical law; it is a precise algebraic identity about a classical polynomial. The proof proceeds by expanding the definition of the quadratic form and simplifying, which the checker verifies step by step. The practical value is that it gives a closed-form expression for the second derivative of CM₃ along a single coordinate, which is exactly what you need when studying how the volume of a tetrahedron responds to small changes in one edge.

The theorem does not claim anything about the full Hessian matrix, which would involve changing two edges at once. It also does not assert that CM₃ is positive for any particular set of lengths; that is a separate question about whether a tetrahedron exists. What it establishes is a sharp, computable fact: the quadratic response to a single-edge perturbation is a pure square term with a coefficient that depends only on the other five lengths. This makes it a useful building block for larger calculations in distance geometry and for the framework's own work on geometric invariants.

theorem cm3_quadratic_singlePerturb (a : SqEdges) (i : Fin 6) (t : ℝ) :
    cm3_quadratic a (singlePerturb i t) =
      cm3_quadratic_coeff i a * t ^ 2 := by
  unfold cm3_quadratic singlePerturb cm3_quadratic_coeff
  fin_cases i <;> simp <;> ring

What this page does not claim

The theorem does not assert that any particular set of six lengths forms a tetrahedron. It does not provide the full Hessian matrix, which requires mixed second derivatives. It does not establish a new physical principle; it is an algebraic identity about a classical polynomial.

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: