Encyclopedia Geometry Geometry Cayley Menger Polynomial Cont Diff Eval

ARTICLE 3 claims 3 theorems

Geometry Cayley Menger Polynomial Cont Diff Eval

A tetrahedron's volume, written as a polynomial in its edge lengths, is smooth enough for every derivative a geometer might need.

Verify this page

A smooth measurement

The Cayley-Menger polynomial is a classical object: for a tetrahedron, it is a fixed polynomial of degree 3 in the six squared edge lengths, and its value equals 288 times the square of the volume. The framework's machine-checked library of formal theorems defines this polynomial explicitly and proves two numerical checkpoints: the unit regular tetrahedron gives 4, and the right-angle unit tetrahedron gives 8, matching the classical volumes √2/12 and 1/6.

The key smoothness result is that this polynomial is Cⁿ for any natural order n. In plain terms, every derivative of the volume-squared function exists and is continuous, no matter how many times you differentiate. The proof builds this from the basic fact that each coordinate projection, reading off one squared edge length, is smooth, and then applies the standard rules for addition, subtraction, and multiplication of smooth functions.

This matters because later work needs second derivatives of the Cayley-Menger expression to study how a tetrahedron's volume responds to small changes in its edges. The theorem guarantees those derivatives exist without case-by-case checking. A separate result shows the polynomial scales as s³ when all squared edge lengths are multiplied by s, which matches the classical volume scaling V → s^{3/2}V.

What the declaration does not claim is just as important. It establishes smoothness of the polynomial, not that the polynomial equals a volume for arbitrary edge data. The identity 288V² = CM₃ holds only for genuine Euclidean tetrahedra, not for arbitrary six numbers that fail the triangle inequalities. The theorem also says nothing about the Regge second-variation coefficient matrix M_ij mentioned in the strategy; that component-by-component comparison remains a target, not a result.

THEOREM cm3_contDiff · IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean
cm3_contDiff · IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean:116 
/-- 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
THEOREM cm3_regular_unit · cm3_rightAngle_unit · IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean
cm3_regular_unit · IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean:79 
/-- The Cayley-Menger value of the unit regular tetrahedron is 4.
Classical: `V_unit_regular = √2 / 12`, so `288 V² = 288 / 72 = 4`. -/
theorem cm3_regular_unit : cm3 regularUnitSqEdges = 4 := by
  unfold cm3 regularUnitSqEdges
  norm_num
cm3_rightAngle_unit · IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean:98 
/-- The Cayley-Menger value of the right-angle unit tetrahedron is 8.
Classical: `V = 1/6`, so `288 V² = 288/36 = 8`. -/
theorem cm3_rightAngle_unit : cm3 rightAngleUnitSqEdges = 8 := by
  unfold cm3 rightAngleUnitSqEdges
  norm_num
THEOREM cm3_scaling · IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean
cm3_scaling · IndisputableMonolith/Geometry/CayleyMengerPolynomial.lean:179 
theorem cm3_scaling (a : SqEdges) (s : ℝ) :
    cm3 (fun e => s * a e) = s ^ 3 * cm3 a := by
  unfold cm3
  ring

What this page does not claim

The polynomial equals 288V² for arbitrary edge data, only for genuine Euclidean tetrahedra. The Regge second-variation coefficient matrix M_ij has been compared component by component to area(f_ij). The declaration proves anything about the physical recognition-to-linking bridge.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND