Geometry Cayley Menger Polynomial Right Angle Unit Sq Edges

A test tetrahedron

The Cayley-Menger determinant is a classical tool from 1841 that answers a geometric question: given six proposed edge lengths, do they actually fit together as a tetrahedron in ordinary Euclidean space? The determinant vanishes exactly when the six lengths are degenerate, and its value is proportional to the square of the tetrahedron's volume. For a tetrahedron, the determinant expands into a fixed polynomial of degree three in the six squared edge lengths, and the classical relation is 288 times the squared volume equals this polynomial.

The machine-checked library of formal theorems defines this polynomial directly as an explicit expression in six variables, then proves two numerical checks. The first check is the regular tetrahedron with all edges of length one, where the polynomial evaluates to 4, matching the classical volume of √2/12. The second check is the right-angle unit tetrahedron, the shape formed by three mutually perpendicular edges of length one meeting at a single vertex, like the corner of a cube sliced off by a plane.

For this right-angle unit tetrahedron, the declaration rightAngleUnitSqEdges assigns the squared lengths: the three edges from the corner get squared length 1, and the three opposite edges, each the hypotenuse of a right triangle with legs 1 and 1, get squared length 2. The theorem cm3_rightAngle_unit proves that the Cayley-Menger polynomial evaluates to 8 for this assignment. This matches the classical volume of 1/6, since 288 times (1/6)² equals 8.

In Recognition Science, this is groundwork for a larger program: the framework models physical space through recognition events, and this polynomial is the workhorse for later derivative and component-comparison theorems. The declaration itself is a definitional choice, not a physical claim. It establishes that the classical polynomial, when applied to this specific edge-length assignment, produces the value that Euclidean geometry requires.

What the declaration does not claim is broader. It does not assert that the right-angle unit tetrahedron is the only shape with these edge lengths, nor does it prove that the polynomial correctly identifies all tetrahedra. It verifies one test point. The theorem is a computational sanity check on a definition, confirming that the explicit polynomial agrees with the classical determinant on this particular shape. The larger claim, that this polynomial drives the physical theory, remains a program under construction.

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

/-- Edge data for the right-angle unit tetrahedron with three orthogonal
unit edges from a single vertex. -/
def rightAngleUnitSqEdges : SqEdges :=
  fun e =>
    match e with
    | ⟨0, _⟩ => 1
    | ⟨1, _⟩ => 1
    | ⟨2, _⟩ => 1
    | ⟨3, _⟩ => 2
    | ⟨4, _⟩ => 2
    | ⟨5, _⟩ => 2
    | ⟨n+6, h⟩ => absurd h (by omega)

/-- The explicit Cayley-Menger polynomial in the six squared edge lengths. -/
def cm3 (a : SqEdges) : ℝ :=
  2 * ( 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 )

What this page does not claim

The right-angle unit tetrahedron is the only shape with these edge lengths. The polynomial is proven to characterize all tetrahedra. The framework derives the Cayley-Menger polynomial from recognition events.

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: