Geometry Freudenthal Cube Triangulation Edge In Tet Iff Local Edge Of

Edge bookkeeping in a triangulated cube

A cube can be divided into six tetrahedra, the simplest solid pieces with triangular faces. One standard way to do this, named for the Dutch mathematician Hans Freudenthal, uses the body diagonal from one corner to the opposite corner and fills the rest with monotone paths between those corners. The result is a triangulation: a way of assembling the cube from tetrahedra that meet only along shared faces, edges, or vertices.

Within this triangulation, each of the six tetrahedra has six edges of its own: three unit-length edges along the cube's sides, two face diagonals, and one body diagonal. But the cube as a whole has 19 distinct edges, because neighboring tetrahedra share edges. The bookkeeping question is simple: when a global edge of the cube lies on a particular tetrahedron, which of that tetrahedron's six local edge slots does it occupy? The declaration edgeInTet_iff_localEdgeOf answers this question completely. It proves, for every global edge and every tetrahedron, that the global edge appears in a given local slot if and only if that global edge is exactly the one the bookkeeping assigns to that slot.

This is a consistency statement, not a geometric discovery. It says the two ways of describing an edge, globally as one of the cube's 19 edges and locally as one of a tetrahedron's six slots, agree with each other perfectly. The theorem is checked by a machine, meaning every case, all 19 times 6 times 6 combinations, has been verified by formal logic. The same library also proves that each local slot is always filled by some global edge, and that the squared length of the local edge matches the squared length of the corresponding global edge.

In the Recognition Science framework, this bookkeeping supports a broader program of building physical geometry from discrete incidence data. The framework models space as a ledger, a discrete record of which pieces touch which. The Freudenthal cube is a concrete test case: a finite, fully specified triangulation where the incidence records can be checked exhaustively. The theorem's role is to certify that the ledger is internally consistent, that no edge is recorded twice in the same tetrahedron and no slot is left empty.

The theorem does not claim that the Freudenthal triangulation is the only way to slice a cube, nor does it say anything about why six tetrahedra are special. It is purely a statement about one chosen triangulation and its bookkeeping. It also does not connect this cube to the framework's forcing chain, the sequence of theorems that derives constants like the golden ratio or the number of spatial dimensions. The cube here is a standalone geometric object, not a step in that derivation.

theorem edgeInTet_iff_localEdgeOf
    (e : Fin 19) (τ f : Fin 6) :
    edgeInTet e τ = some f ↔ e = localEdgeOf τ f := by
  fin_cases e <;> fin_cases τ <;> fin_cases f <;>
    simp [edgeInTet, localEdgeOf]

theorem localEdge_complete (τ f : Fin 6) :
    ∃ e : Fin 19, edgeInTet e τ = some f := by
  exact ⟨localEdgeOf τ f, (edgeInTet_iff_localEdgeOf (localEdgeOf τ f) τ f).2 rfl⟩

theorem local_sqEdge_eq_global
    (e : Fin 19) (τ f : Fin 6) (h : edgeInTet e τ = some f) :
    freudenthalTet.sqEdge f = globalSqEdge e := by
  fin_cases e <;> fin_cases τ <;> fin_cases f <;>
    simp [edgeInTet, freudenthalTet, freudenthalTetSqEdges, globalSqEdge] at h ⊢

What this page does not claim

The Freudenthal triangulation is the only way to slice a cube into tetrahedra. This theorem connects the cube to the framework's forcing chain that derives constants like the golden ratio. The six tetrahedra are special in any physical sense beyond being one valid decomposition.

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: