IndisputableMonolith.Geometry.FreudenthalCubeTriangulation
Defines the Freudenthal triangulation of the unit cube: six tetrahedra whose squared edge lengths are three unit steps, two face diagonals, and one body diagonal. Supplies the local edge-slot incidence data (vertices, local-to-global edge maps, membership lemmas) used by multi-cube strips, periodic tori, and Schläfli length-chain certificates. Mostly definitional scaffolding with elementary incidence equalities.
claimOn the unit cube, the Freudenthal decomposition yields six tetrahedra. For each tetrahedron the ordered squared-edge 6-tuple is $(1,1,1,2,2,3)$: three axis-aligned unit edges, two face diagonals of squared length $2$, and one space diagonal of squared length $3$. The module records the vertex sets, the local-to-global edge map, and the incidence relation between edges and tetrahedra.
background
Recognition Science geometry works in the discrete Regge setting: a 3-manifold is triangulated into tetrahedra whose edge lengths determine dihedral angles and deficit angles. The first variation of the nonlinear Regge action at a flat conformal background vanishes by Schläfli cancellation plus zero deficit (module ReggeActionFirstVariation).
The Freudenthal (or Kuhn) triangulation is the standard way to cut the unit cube into six congruent tetrahedra so that face triangulations match across shared faces. Each tetrahedron carries a fixed squared-edge signature: three edges of length $1$, two of length $\sqrt{2}$, one of length $\sqrt{3}$. The module names this local 6-tuple and the combinatorial maps (edge vertices, tetrahedron vertices, local edge index to global squared length) needed to assemble larger meshes without double-counting shared edges.
proof idea
Definition module. It introduces the constant squared-edge tuple for a Freudenthal tetrahedron, the six tetrahedra of the unit cube, and the incidence predicates relating local edge slots to global edges and vertices. Supporting lemmas are elementary equalities and biconditionals (local edge equals global squared length; edge lies in a tetrahedron iff it is one of its six local edges; vertex sets match). No analytic or variational argument lives here.
why it matters in Recognition Science
This is the atomic geometric cell for every multi-cube Freudenthal construction in the stack. FreudenthalTwoCubeStrip imports it to glue two cubes across a face and prove the global edge-slot partition after deduplicating five shared edges. PeriodicFreudenthalTorus lifts the same local data to a typed periodic vertex/edge/tetrahedron model whose finite encodings satisfy the IncidenceEdgeSlotPartition required by the nonlinear Regge first-variation theorem. Gravity.FreudenthalLengthChainEndpointCert evaluates the full $6\times 6$ Schläfli poly-summand table and the closed-form dihedral length derivatives exactly on freudenthalTetSqEdges. Without this local signature the length-chain certificates and the multi-cube incidence proofs have no concrete edge data.
scope and limits
- Does not prove vanishing of the Regge first variation; only supplies local edge data.
- Does not construct multi-cube or periodic meshes; those live in downstream modules.
- Does not compute dihedral angles or Schläfli summands; only the squared-edge 6-tuple.
- Does not address continuum limits or non-Freudenthal triangulations.
- Does not claim uniqueness of the cube decomposition among all six-tet triangulations.
used by (3)
depends on (1)
declarations in this module (16)
-
def
freudenthalTetSqEdges -
theorem
cm3_freudenthalTetSqEdges -
def
freudenthalTet -
def
edgeVerts -
def
globalSqEdge -
def
tetVerts -
def
localEdgeOf -
def
edgeInTet -
def
freudenthalCube -
theorem
edgeInTet_iff_localEdgeOf -
theorem
local_sqEdge_eq_global -
theorem
edgeInTet_vertices -
theorem
localEdge_complete -
def
freudenthalCube_incidenceConsistent -
def
freudenthalCube_edgeSlotPartition -
def
freudenthalCube_edgeSlotBookkeeping