Geometry Cayley Menger Polynomial Cm3 Cont Diff

Smoothness of the Cayley-Menger polynomial

The Cayley-Menger polynomial is a classical object in geometry: a single algebraic expression in the six squared edge lengths of a tetrahedron whose value equals 288 times the square of the tetrahedron's volume. For a genuine Euclidean tetrahedron, the relationship is exact: 288·V² equals the polynomial. This polynomial is the standard tool for deciding whether six lengths can form a tetrahedron and for computing volume without coordinates.

The declaration cm3_contDiff establishes a smoothness property: the polynomial is Cⁿ for every natural number n, meaning it has continuous derivatives of every order. In plain terms, the polynomial has no corners, jumps, or singularities anywhere in the six-dimensional space of squared edge lengths. The proof is built directly from the fact that addition, subtraction, and multiplication are smooth operations, combined with the fact that each edge length projection is smooth. The machine-checked library of formal theorems verifies this by explicit construction using standard smoothness combinators.

Why does this matter? Later work in the framework needs second derivatives of the Cayley-Menger polynomial, for example to compare the Regge second-variation coefficient matrix with area terms. The smoothness theorem guarantees that such derivatives exist and are continuous, so the later component-by-component comparisons are mathematically legitimate. The theorem also yields an immediate corollary: the polynomial is continuous, which is a useful basic fact for any geometric argument.

In Recognition Science, the framework models physical structure through a discrete ledger of recognition events, but this particular declaration is purely classical geometry. It does not invoke recognition, cost, or any framework-specific concept. It is a standalone result about a standard polynomial, verified in the machine-checked library, and it provides a foundation for later derivative computations within the framework's geometric program.

/-- The Cayley-Menger polynomial is `Cⁿ` for any natural order `n`.
Built explicitly from `ContDiff.add`, `ContDiff.sub`, `ContDiff.mul`. -/
theorem cm3_contDiff (n : ℕ∞) : ContDiff ℝ n cm3 := by
  have h0 := contDiff_eval n 0
  have h1 := contDiff_eval n 1
  have h2 := contDiff_eval n 2
  have h3 := contDiff_eval n 3
  have h4 := contDiff_eval n 4
  have h5 := contDiff_eval n 5
  have hconst : ContDiff ℝ n (fun _ : SqEdges => (2 : ℝ)) := contDiff_const
  -- Build linear combinations.
  have s1 : ContDiff ℝ n (fun a : SqEdges => a 1 + a 2 + a 3 + a 4 - a 0 - a 5) :=
    ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add (ContDiff.add h1 h2) h3) h4) h0) h5
  have s2 : ContDiff ℝ n (fun a : SqEdges => a 0 + a 2 + a 3 + a 5 - a 1 - a 4) :=
    ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add (ContDiff.add h0 h2) h3) h5) h1) h4
  have s3 : ContDiff ℝ n (fun a : SqEdges => a 0 + a 1 + a 4 + a 5 - a 2 - a 3) :=
    ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add (ContDiff.add h0 h1) h4) h5) h2) h3
  -- Three "balanced" cubic terms.
  have c1 : ContDiff ℝ n (fun a : SqEdges =>
      a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)) :=
    ContDiff.mul (ContDiff.mul h0 h5) s1
  have c2 : ContDiff ℝ n (fun a : SqEdges =>
      a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)) :=
    ContDiff.mul (ContDiff.mul h1 h4) s2
  have c3 : ContDiff ℝ n (fun a : SqEdges =>
      a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)) :=
    ContDiff.mul (ContDiff.mul h2 h3) s3
  -- Four monomial cubic terms.
  have nA : ContDiff ℝ n (fun a : SqEdges => a 0 * a 1 * a 3) :=
    ContDiff.mul (ContDiff.mul h0 h1) h3
  have nB : ContDiff ℝ n (fun a : SqEdges => a 0 * a 2 * a 4) :=
    ContDiff.mul (ContDiff.mul h0 h2) h4
  have nC : ContDiff ℝ n (fun a : SqEdges => a 1 * a 2 * a 5) :=
    ContDiff.mul (ContDiff.mul h1 h2) h5
  have nD : ContDiff ℝ n (fun a : SqEdges => a 3 * a 4 * a 5) :=
    ContDiff.mul (ContDiff.mul h3 h4) h5
  have inner : ContDiff ℝ n (fun a : SqEdges =>
        a 0 * a 5 * (a 1 + a 2 + a 3 + a 4 - a 0 - a 5)
      + a 1 * a 4 * (a 0 + a 2 + a 3 + a 5 - a 1 - a 4)
      + a 2 * a 3 * (a 0 + a 1 + a 4 + a 5 - a 2 - a 3)
      - a 0 * a 1 * a 3
      - a 0 * a 2 * a 4
      - a 1 * a 2 * a 5
      - a 3 * a 4 * a 5 ) :=
    ContDiff.sub (ContDiff.sub (ContDiff.sub (ContDiff.sub
      (ContDiff.add (ContDiff.add c1 c2) c3) nA) nB) nC) nD
  show ContDiff ℝ n cm3
  unfold cm3
  exact ContDiff.mul hconst inner

/-- An immediate corollary: `cm3` is continuous. -/
theorem cm3_continuous : Continuous cm3 :=
  (cm3_contDiff 0).continuous

What this page does not claim

The declaration does not prove that the polynomial is analytic or that it has derivatives of infinite order in the sense of real analyticity. The declaration does not establish that the polynomial is positive or that it characterizes Euclidean tetrahedra; it only establishes smoothness. The declaration does not involve recognition, cost, or any framework-specific concept; it is a purely classical geometric result.

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: