Geometry Cayley Menger Derivatives Has Deriv At Cm3 Partial1

The partial derivative theorem

The Cayley-Menger polynomial is the algebraic test for whether six edge lengths can form a tetrahedron in ordinary three-dimensional space. For a candidate set of squared edge lengths, the polynomial vanishes exactly when the lengths are geometrically consistent. The theorem hasDerivAt_cm3_partial1 concerns the first of the six edges: it states that, at any choice of the six squared lengths, the polynomial changes smoothly as that one edge length varies, and it gives the exact rate of change in closed form.

The rate of change is a quadratic polynomial in the six squared lengths, written explicitly in the framework's library. The theorem is proved by a machine-checked computation: it expands the polynomial after a small change to one edge, isolates the linear term, and verifies that the remainder vanishes in the limit. This is a local statement about a single edge; it does not require the six lengths to form a valid tetrahedron, and it says nothing about how the other five edges respond.

In Recognition Science, this derivative is a stepping stone. The framework models a discrete ledger, a record of recognition events, whose geometric content is carried by such polynomials. The derivative feeds into a second-variation matrix that the framework compares with triangle areas. The theorem supplies the formal foundation: without a proved derivative, that comparison would rest on an unverified assumption.

The theorem does not claim that the six lengths form a tetrahedron, nor that the polynomial's value is zero. It claims only that the function is differentiable in one coordinate, and it names the derivative. That distinction matters: a derivative can exist at points where the geometric condition fails, just as a curve can have a slope where it crosses zero.

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

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

What this page does not claim

The theorem does not assert that the six edge lengths form a valid tetrahedron. The theorem does not provide the derivative with respect to more than one edge at a time. The theorem does not establish the second-variation matrix or any comparison with triangle areas; it only supplies a partial derivative used in that later construction.

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: