Geometry Freudenthal Cube Triangulation Freudenthal Cube Edge Slot Partition

The edge-slot partition

The Freudenthal triangulation of a cube is the standard decomposition of a unit cube into six tetrahedra, using the body diagonal from one corner to the opposite corner. Each tetrahedron is a monotone path from one end of that diagonal to the other, and the vertices are labeled by binary coordinates: 0 is (0,0,0), 7 is (1,1,1), and the other six corners are the remaining combinations of 0 and 1. This is a classical construction in computational geometry, used in finite element meshes and volume rendering.

Each of the six tetrahedra has six edges: three unit step edges, two face diagonals, and one body diagonal. The 19 unique edges of the whole triangulation are the cube's 12 edges, its 6 face diagonals, and the single body diagonal. The declaration freudenthalCube_edgeSlotPartition establishes, in a machine-checked library of formal theorems, that this bookkeeping is consistent: every one of the 36 local edge slots across the six tetrahedra maps to exactly one of the 19 global edges, and no slot is duplicated or left out. It proves that the incidence map from a global edge and a tetrahedron to a local slot is a bijection onto the slots of that tetrahedron, and that the squared lengths agree between the local and global views.

In Recognition Science, this is a concrete instance of the framework's ledger, a discrete record of events and their relations. The framework models geometric triangulations as such ledgers, and this declaration is the bookkeeping that makes the Freudenthal cube a valid instance of the framework's incidence class. The declaration also proves the tetrahedra are nondegenerate, meaning they have positive volume, and that the whole cube triangulation is incidence-consistent.

What the declaration does not claim is also precise. It does not assert that this is the only way to triangulate a cube, nor that the Freudenthal triangulation is optimal in any sense. It does not derive any physical law or constant; it is purely a piece of combinatorial geometry. The declaration is a definitional choice, a model of the cube, not a theorem about the physical world.

/-- The Freudenthal cube has the intended unique/no-duplication local edge-slot
partition. -/
def freudenthalCube_edgeSlotPartition :
    IncidenceEdgeSlotPartition freudenthalCube freudenthalCube_incidenceConsistent where
  localEdgeOf := localEdgeOf
  edgeInTet_iff := by
    intro e τ f
    exact edgeInTet_iff_localEdgeOf e τ f

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

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

What this page does not claim

This is the only possible triangulation of a cube. The Freudenthal triangulation is optimal by any metric. Any physical law or constant is derived from this declaration.

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: