Geometry Freudenthal Cube Triangulation Cm3 Freudenthal Tet Sq Edges

The six-tetrahedron cube

The Freudenthal triangulation is a standard way to divide a cube into tetrahedra. Label the eight corners of a unit cube by binary coordinates, from 0 at (0,0,0) to 7 at (1,1,1). Draw the body diagonal from corner 0 to corner 7. The six tetrahedra are then the monotone paths along the cube's edges from 0 to 7, one for each of the six possible orderings of the three coordinate steps. This decomposition appears in computational geometry and finite element methods because it respects the cube's grid structure.

Each of the six tetrahedra has the same edge lengths: three edges of length 1 (the unit steps), two face diagonals of squared length 2, and one body diagonal of squared length 3. The squared edge lengths are recorded in the tuple (1, 2, 3, 1, 2, 1). A classical test called the Cayley-Menger determinant decides whether six edge lengths can form a nondegenerate tetrahedron, one with positive volume rather than a flat triangle. For this tuple the determinant equals 8, a positive number, which proves the tetrahedron is genuine.

In Recognition Science, the framework's machine-checked library of formal theorems records this fact as the declaration cm3_freudenthalTetSqEdges. The theorem states that the Cayley-Menger determinant for the Freudenthal tetrahedron's squared edge lengths equals 8. The proof is computational: it unfolds the definition of the determinant and evaluates the arithmetic. The same file also defines the full triangulation with its 8 vertices, 19 edges, and 6 tetrahedra, and proves that the local edge bookkeeping is consistent with the global geometry.

What the declaration does not claim is broader. It does not assert that the Freudenthal triangulation is the only way to cut a cube into tetrahedra, nor that the Cayley-Menger value 8 has any special physical meaning. The number 8 is simply the determinant for this particular edge tuple. The theorem also says nothing about the Recognition Science forcing chain or the golden ratio; it is a standalone geometric fact about a classical construction.

theorem cm3_freudenthalTetSqEdges :
    CayleyMengerPolynomial.cm3 freudenthalTetSqEdges = 8 := by
  unfold freudenthalTetSqEdges CayleyMengerPolynomial.cm3
  norm_num

/-- The local squared-edge tuple for every Freudenthal tetrahedron in the unit
cube: three unit step edges, two face diagonals, and one body diagonal. -/
def freudenthalTetSqEdges : CayleyMengerPolynomial.SqEdges
  | 0 => 1
  | 1 => 2
  | 2 => 3
  | 3 => 1
  | 4 => 2
  | 5 => 1

What this page does not claim

The Freudenthal triangulation is not claimed to be the only cube decomposition. The Cayley-Menger value 8 carries no physical or framework-specific meaning beyond the determinant for this edge tuple. The declaration does not connect to the golden ratio or the Recognition Science 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/FreudenthalCubeTriangulation.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: