freudenthalCube
plain-language theorem explainer
Packages the classical Freudenthal decomposition of the unit cube into six tetrahedra as a concrete 3D triangulation: 8 binary-labeled vertices, 19 edges, 6 tets, with explicit endpoint, vertex-list, and edge-in-tet incidence maps. Discrete-geometry and Regge-calculus work on the cube cites this as the base combinatorial instance. The body is a pure structure fill-in wiring precomputed tables and a single nondegenerate tet template on every cell.
Claim. The Freudenthal cube is the finite triangulation of the unit cube with $8$ vertices (binary labels $0=\!(0,0,0),\ldots,7=\!(1,1,1)$), $19$ edges, and $6$ tetrahedra given by the monotone paths from $0$ to $7$, equipped with the edge-endpoint map, the tetrahedron vertex lists, the global-edge-to-local-slot incidence, and a common nondegenerate squared-edge assignment on each tetrahedron.
background
The module builds incidence bookkeeping for the standard Freudenthal split of one unit cube into six tetrahedra along the body diagonal from vertex $0$ to vertex $7$. Cube vertices are binary coordinates: $0=(0,0,0)$, $1=(1,0,0)$, $2=(0,1,0)$, $3=(1,1,0)$, $4=(0,0,1)$, $5=(1,0,1)$, $6=(0,1,1)$, $7=(1,1,1)$. The six tetrahedra are exactly the monotone paths from $0$ to $7$.
Upstream tables supply the combinatorial data. edgeVerts lists the $19$ unique undirected edges as pairs in $\mathrm{Fin},8\times\mathrm{Fin},8$. tetVerts lists each of the six tets as an ordered $4$-tuple of cube vertices. edgeInTet is the partial incidence map from a global edge index and a tet index to a local edge slot in $\mathrm{Fin},6$ when the edge belongs to that tet. freudenthalTet is a single nondegenerate tetrahedron (positive squared edge lengths and positive Cayley-Menger volume) reused as the metric template on every cell.
The ambient type is a $3$D triangulation record: vertex/edge/tet counts plus those three incidence maps and a per-tet nondegeneracy witness. The module imports the first-variation Regge-action layer, so this instance is the combinatorial substrate for discrete curvature on the cube.
proof idea
Pure definitional instance of the $3$D triangulation record. Counts are hard-coded ($n_V=8$, $n_E=19$, $n_T=6$). The three incidence fields are the module-local tables edgeVerts, tetVerts, and edgeInTet. The per-tet field is the constant map sending every tet index to the shared nondegenerate template freudenthalTet. No tactics and no lemmas: just structure field assignment.
why it matters
This is the named combinatorial object that all subsequent Freudenthal-cube incidence lemmas quantify over. Downstream, freudenthalCube_incidenceConsistent packages global squared-edge lengths and the vertex-consistency of edgeInTet; freudenthalCube_edgeSlotPartition installs the unique local-slot partition via localEdgeOf; and freudenthalCube_edgeSlotBookkeeping assembles those into the full edge-slot bookkeeping bundle used by discrete first-variation arguments.
In the Recognition geometry stack this is the unit-cell triangulation behind Regge-type action and first-variation identities on the cube (the module imports the Regge first-variation layer). It does not itself touch the forcing chain (T0-T8), the J-cost, or the phi ladder; it is pure discrete geometry scaffolding that later continuum or recognition-length arguments can instantiate on a single cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.