Geometry Tetrahedron Realization Sq Edge Of Points

Squared edge lengths

A tetrahedron is a pyramid with four triangular faces, six edges, and four vertices. In Euclidean geometry, you can describe such a shape either by listing the coordinates of its four corner points or by giving the six edge lengths. The second description is often more useful because it does not depend on where the shape sits in space. This page concerns a formal bridge between those two descriptions: a definition called sqEdgeOfPoints that takes four points in three-dimensional Euclidean space and returns the six squared edge lengths.

The definition is part of a machine-checked library of formal statements. It works by first pairing each of the six edges with its two endpoint vertices, then computing the vector from one endpoint to the other, and finally taking the squared length of that vector. The result is a list of six real numbers, one for each edge, in a fixed order. The squared length, rather than the length itself, is used because it avoids square roots and keeps the arithmetic simple for later proofs.

One immediate property is proved: every squared edge length is nonnegative. This follows directly from the fact that a squared real number is never negative. The definition also serves as the input to two different formulas for the volume of the tetrahedron. One formula uses the Gram matrix of vectors from a single vertex; the other uses the Cayley-Menger determinant built from the six edge lengths. A stated target, called GramCayleyMengerVolumeTheorem, asserts that these two volume formulas agree for any realized tetrahedron. That target is declared but not yet proved in the library.

In Recognition Science, this definition is a small but necessary step in a larger program. The framework derives physical structure from a ledger of recognition events, and it treats conventional geometry as itself derived. Here, the definition connects the abstract six-coordinate edge data to concrete points in Euclidean space, with a nondegeneracy condition requiring that the four points are affinely independent, meaning they do not lie in a plane. This condition is what will later support proofs about positive volume and strict dihedral angles.

What the definition does not claim is broader than what it does. It does not prove that any six numbers form a valid tetrahedron; that is a separate existence question. It does not establish the volume equality, which remains an open target. And it does not by itself say anything about the recognition ledger or the forcing chain; it is a geometric utility, not a physical law.

/-- Extract the six squared edge lengths in the same order as `SqEdges`. -/
def sqEdgeOfPoints (T : RealizedTet) : SqEdges :=
  fun e =>
    let v := edgeVertices3 e
    vertexSqDist T v.1 v.2

/-- Squared edge lengths from points are nonnegative. -/
theorem sqEdgeOfPoints_nonneg (T : RealizedTet) (e : Fin 6) :
    0 ≤ sqEdgeOfPoints T e := by
  unfold sqEdgeOfPoints vertexSqDist
  exact sq_nonneg _

What this page does not claim

The definition does not prove that any six numbers form a valid tetrahedron. The volume equality between Gram and Cayley-Menger formulas remains an open target, not a proved theorem. The definition itself says nothing about the recognition ledger or the forcing chain.

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