Geometry Realisability Cone

The realisability cone

A tetrahedron is a solid with four triangular faces, six edges, and four vertices. Given six positive numbers intended as squared edge lengths, the numbers may or may not describe an actual tetrahedron in ordinary three-dimensional space. The condition is not just that each length is positive: the six numbers must also satisfy a determinantal inequality known as the Cayley-Menger condition, which encodes the requirement that the four vertices can be placed with the prescribed mutual distances. The set of all six-tuples that pass this test is the realisability cone: a cone because scaling all six squared lengths by the same positive factor preserves realisability, and open because strict positivity is required on both the edge lengths and the determinant.

The classical criterion goes back to the work of Arthur Cayley and Karl Menger in the early twentieth century. For a triangle, three positive numbers are realisable exactly when each is less than the sum of the other two, the triangle inequality. For a tetrahedron the condition is more subtle: the Cayley-Menger determinant, built from the six squared edge lengths, must be positive. That determinant vanishes when the four points lie in a plane, and it becomes negative when the lengths are mutually inconsistent. The cone is therefore the natural domain on which tetrahedral geometry formulas, such as the dihedral-angle formula, are valid.

In Recognition Science, the framework's machine-checked library of formal theorems defines this cone precisely. The definition, RealisableTetCone, is the set of six-tuples of squared edge lengths with every entry positive and with the Cayley-Menger determinant positive. The library proves two membership facts: the regular unit tetrahedron, whose six edges all have length one, lies in the cone; and the right-angle unit tetrahedron, with three mutually perpendicular unit edges, also lies in the cone. These are sanity checks that the cone is nonempty and contains the two most familiar tetrahedra.

The cone matters because it is the domain on which later geometric formulas are intended to be used. The framework's library states that the tetrahedral Cayley-Menger and dihedral-angle formulas are meant for this open domain. The two membership theorems guarantee that the domain is not empty and that the standard reference tetrahedra are admissible inputs. A reader can now see that the cone is not an abstract curiosity: it is the precise collection of length data for which the framework's tetrahedral geometry is defined.

/-- Basic open tetrahedral cone: positive squared edge lengths and positive
Cayley-Menger determinant.  Later phases strengthen this with face-minor
positivity as needed by cofactor denominators. -/
def RealisableTetCone : Set SqEdges :=
  {a | (∀ i : Fin 6, 0 < a i) ∧ 0 < cm3 a}

/-- The regular unit tetrahedron lies in the basic realisability cone. -/
theorem regularUnit_mem_realisableTetCone :
    regularUnitSqEdges ∈ RealisableTetCone := by
  constructor
  · intro i
    unfold regularUnitSqEdges
    norm_num
  · rw [cm3_regular_unit]
    norm_num

/-- The right-angle unit tetrahedron lies in the basic realisability cone. -/
theorem rightAngleUnit_mem_realisableTetCone :
    rightAngleUnitSqEdges ∈ RealisableTetCone := by
  constructor
  · intro i
    unfold rightAngleUnitSqEdges
    fin_cases i <;> norm_num
  · rw [cm3_rightAngle_unit]
    norm_num

What this page does not claim

The cone is not claimed to characterize all realisable tetrahedra beyond the two stated inequalities. No claim is made about the dihedral-angle formula's validity outside this open domain. The framework's recognition theory is not invoked in this module.

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/RealisabilityCone.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: