Geometry Realisability Cone Regular Unit Mem Realisable Tet Cone

The basic realisability cone

A tetrahedron is a pyramid with a triangular base, four triangular faces, and six edges. For a set of six lengths to form a tetrahedron at all, the lengths cannot be arbitrary: they must satisfy inequalities that rule out flat or impossible shapes. One classical test is the Cayley-Menger determinant, a formula built from the squared edge lengths that measures whether the six lengths can come from a tetrahedron in Euclidean space. When the determinant is positive, the lengths pass this test; when it is zero or negative, the configuration collapses or cannot exist.

The framework's library, a machine-checked collection of formal theorems, defines the basic realisability cone as the set of all squared edge lengths that are positive and have a positive Cayley-Menger determinant. This cone is the open domain on which the tetrahedral formulas are intended to be used. The declaration regularUnit_mem_realisableTetCone proves that the regular unit tetrahedron, the shape with all six edges of length 1, lies in this cone. The proof is direct: it checks that each of the six squared edge lengths equals 1, hence is positive, and that the Cayley-Menger determinant for this shape is positive.

This result is a recognition event in the framework's sense: a discrete record that a particular configuration passes a structural test. The test here is geometric, not physical: it says the regular unit tetrahedron is admissible as a tetrahedron, not that it is the only such shape or that any other property follows. The right-angle unit tetrahedron, with edges of length 1, 1, and √2 in the right places, also lies in the cone by a similar proof.

What the declaration does not claim is just as important. It does not prove that the regular unit tetrahedron is the only member of the cone, nor that the cone contains every possible tetrahedron. The cone is defined by two conditions, positivity of edges and positivity of the determinant; the declaration confirms one specific shape satisfies both. It also does not address whether the Cayley-Menger determinant being positive is sufficient for a tetrahedron to exist, only that this particular shape passes the test. The result is a building block for later phases that strengthen the cone with face-minor positivity, as the docstring notes.

The practical upshot is that the framework has a verified starting point for tetrahedral geometry: a concrete, checkable example that the realisability cone is nonempty. This matters because the cone is the domain on which further formulas, such as dihedral-angle computations, are meant to operate. With the regular unit tetrahedron confirmed inside, those formulas have a known-good input to test against, and the framework can build outward from a solid geometric base.

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

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

What this page does not claim

The declaration does not prove that the regular unit tetrahedron is the only member of the cone. It does not show that a positive Cayley-Menger determinant alone is sufficient for realisability. It makes no claim about the physical existence of tetrahedra in space, only about the formal cone.

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: