Geometry Realisability Cone Realisable Tet Cone

The tetrahedral cone

A tetrahedron is a pyramid with a triangular base, the simplest three-dimensional solid. Its shape is fixed by six edge lengths, the three edges of the base and the three edges running up to the apex. Not every choice of six positive numbers forms a real tetrahedron: the lengths must obey constraints, just as three numbers form a triangle only when each is less than the sum of the other two. The classical test for a tetrahedron is the Cayley-Menger determinant, a quantity built from the six squared edge lengths that is positive exactly when the lengths can be realized as an ordinary tetrahedron in Euclidean space.

The declaration RealisableTetCone defines the set of squared edge lengths that pass this test: all six squared lengths are positive, and the Cayley-Menger determinant is positive. This is the recognition cone, a region in six-dimensional space where the framework's geometry formulas are intended to operate. The declaration proves two membership facts: the regular unit tetrahedron, with all edges equal to one, lies in the cone, and so does the right-angle unit tetrahedron, whose three edges meeting at one vertex are mutually perpendicular. Both are verified by direct computation of the determinant.

The definition is deliberately basic. It requires only positive edge lengths and a positive determinant, but it does not yet impose the stronger condition that every triangular face itself satisfies the triangle inequality. That stronger condition, called face-minor positivity, is left for later phases, where it will be needed as a denominator in cofactor formulas. The cone is therefore an open domain for future work, not a complete characterization of every possible tetrahedron.

What the declaration does not claim is equally precise. It does not assert that every point in the cone corresponds to a tetrahedron; the positive determinant is a necessary condition, and the full realisability criterion may require additional face conditions. It does not prove that the cone is nonempty beyond the two named examples. And it makes no statement about the framework's physical constants or forcing chain; this is a purely geometric definition, a foundation stone for later formulas rather than a result about recognition costs or particle masses.

/-- 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 does not yet prove that every point in it is a realisable tetrahedron. The declaration makes no claim about the framework's physical constants or forcing chain. Face-minor positivity is not part of this basic definition.

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: