Geometry Cayley Menger Derivatives Has Deriv At Cm3 Partial0

The single-edge derivative

The Cayley-Menger polynomial is a classical object in geometry: a formula in the six squared edge lengths of a tetrahedron whose vanishing tells you whether those six lengths can actually form a tetrahedron in three-dimensional space. For a tetrahedron with vertices labeled 0 through 3, the edges are numbered in a fixed convention: edge 0 connects vertices 0 and 1, edge 1 connects 0 and 2, and so on up to edge 5 connecting 2 and 3. The polynomial itself is a cubic expression in these six squared lengths, and it encodes the volume of the tetrahedron: its value is proportional to the square of the volume, so it vanishes exactly when the tetrahedron is flat or degenerate.

What the declaration hasDerivAt_cm3_partial0 establishes is a precise statement about how this polynomial responds when you change just one of those six lengths. Fix a tetrahedron, keep five of its squared edge lengths fixed, and let the sixth one, edge 0, vary continuously. The theorem says that the polynomial is differentiable with respect to that single variable, and it gives the derivative explicitly: the derivative equals a specific quadratic polynomial in the six squared lengths, which the framework writes as cm3_partial0. In plain terms, if you know the current six lengths, you can compute exactly how fast the polynomial changes as you nudge edge 0, and that rate of change is itself a simple polynomial expression, not a complicated limit or an approximation.

The result is not a numerical fact about any particular tetrahedron. It is a general statement that holds for every choice of the six squared edge lengths, because the proof works by expanding the polynomial symbolically and checking that the derivative formula matches the definition of differentiability. The same pattern repeats for each of the other five edges, giving six separate theorems, one per edge. Together they form the gradient of the Cayley-Menger polynomial, the vector of all six partial derivatives, which the framework assembles into a single object called cm3_grad, the list of all six rates of change.

In Recognition Science, this derivative is a stepping stone, not a destination. The framework's library of machine-checked formal theorems uses these partial derivatives to build the Regge second-variation matrix, an object that measures how the polynomial curves as you move several edges at once. That matrix is later compared with the areas of the tetrahedron's faces through a chain rule and a conformal edge ansatz, a specific choice of how the edge lengths scale together. The differentiability theorem for a single edge is what makes that chain rule legal: without knowing that each individual partial derivative exists and has the stated closed form, the later comparison would lack a rigorous foundation.

What the theorem does not claim is just as important as what it proves. It does not say that the Cayley-Menger polynomial is differentiable as a function of all six variables at once, though that stronger statement is true and is proved elsewhere in the library. It does not assert anything about the geometry of actual tetrahedra, such as whether a given set of lengths forms a valid shape; the polynomial's vanishing condition is a separate matter. And it does not by itself establish any result about the Regge matrix or the conformal ansatz, which require additional theorems to connect the derivatives to those objects. The single-edge derivative is a precise, narrow tool, and the framework uses it exactly where it is needed.

/-- The closed-form `cm3_partial0` is the derivative of `t ↦ cm3 (a.update 0 t)`
at `t = a 0`. -/
theorem hasDerivAt_cm3_partial0 (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cm3 (Function.update a 0 t)) (cm3_partial0 a) (a 0) := by
  simpa [cm3_grad] using hasDerivAt_cm3_grad a 0

theorem hasDerivAt_cm3_partial1 (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cm3 (Function.update a 1 t)) (cm3_partial1 a) (a 1) := by
  simpa [cm3_grad] using hasDerivAt_cm3_grad a 1

theorem hasDerivAt_cm3_partial2 (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cm3 (Function.update a 2 t)) (cm3_partial2 a) (a 2) := by
  simpa [cm3_grad] using hasDerivAt_cm3_grad a 2

theorem hasDerivAt_cm3_partial3 (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cm3 (Function.update a 3 t)) (cm3_partial3 a) (a 3) := by
  simpa [cm3_grad] using hasDerivAt_cm3_grad a 3

theorem hasDerivAt_cm3_partial4 (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cm3 (Function.update a 4 t)) (cm3_partial4 a) (a 4) := by
  simpa [cm3_grad] using hasDerivAt_cm3_grad a 4

theorem hasDerivAt_cm3_partial5 (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cm3 (Function.update a 5 t)) (cm3_partial5 a) (a 5) := by
  simpa [cm3_grad] using hasDerivAt_cm3_grad a 5

What this page does not claim

The theorem does not establish differentiability of the polynomial as a function of all six variables at once. It does not assert anything about whether a given set of edge lengths forms a valid tetrahedron. It does not by itself prove any property of the Regge second-variation matrix or the conformal ansatz.

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: