Geometry Cayley Menger Polynomial Cm3 Right Angle Unit

The right-angle test

The Cayley-Menger formula is a classical way to compute the volume of a simplex, such as a tetrahedron, from its edge lengths alone. For a tetrahedron with vertices 0, 1, 2, and 3, the formula takes the six squared edge lengths and produces a number related to the volume. The specific polynomial used here is degree 3 in those six squared lengths, and the classical relation is 288 times the squared volume equals the polynomial's value.

One test case is the right-angle unit tetrahedron, the shape formed by three mutually perpendicular edges of length 1 meeting at one vertex. Its volume is 1/6, a fact known since the ancient Greeks. The machine-checked theorem cm3_rightAngle_unit verifies that the explicit Cayley-Menger polynomial, when fed the squared edge lengths of this shape (1, 1, 1, 2, 2, 2), returns the value 8. Since 288 times (1/6)² equals 8, the theorem confirms the polynomial reproduces the known volume.

This is a numerical check on two specific test points, not a general proof. The purpose is to build a rigorous foundation for comparing the Regge second-variation coefficient matrix against the area of faces, a deeper program. The theorem itself only establishes the polynomial's value at this one configuration, and it does not claim the polynomial gives the volume for any tetrahedron, nor does it prove the general Cayley-Menger relation.

In Recognition Science, this theorem is a small but necessary step. It provides a concrete, verified anchor point for a polynomial that will later be used in derivative and component-comparison theorems. The framework models geometric structures through such explicit, machine-checked calculations, building confidence one test case at a time.

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

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

What this page does not claim

The theorem does not prove the Cayley-Menger formula for all tetrahedra. The theorem does not establish any property of the Regge second-variation matrix. The theorem does not relate the polynomial to the Recognition Science framework's deeper structure.

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: