freudenthalTet
plain-language theorem explainer
The unit-cube Freudenthal tetrahedron (three unit edges, two face diagonals, one body diagonal) is recorded as a nondegenerate tet in the Cayley-Menger sense. Builders of the six-tet cube triangulation, two-cube strips, and periodic Freudenthal tori cite it as the local geometric atom. Nondegeneracy is a short positivity check: edge squares by case split, volume via the precomputed Cayley-Menger value 8.
Claim. The Freudenthal tetrahedron of the unit cube, with squared edge lengths given by three unit steps, two face diagonals ($2$), and one body diagonal ($3$), is nondegenerate: every squared edge length is positive and the Cayley-Menger cubic of those lengths is positive.
background
The module builds the standard Freudenthal decomposition of one unit cube into six tetrahedra along the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Cube vertices are binary coordinate labels; the six tets are the monotone lattice paths from $0$ to $7$.
A nondegenerate tetrahedron is a squared-edge tuple with every entry positive and with positive Cayley-Menger cubic $\mathrm{cm}_3$. The local length table for every Freudenthal tet in the unit cube is fixed once and for all: three unit step edges, two face diagonals, and one body diagonal. Upstream, that table evaluates to $\mathrm{cm}_3=8$.
proof idea
Definitional package of a nondegenerate tet whose squared-edge field is the Freudenthal local table. Edge positivity: introduce the edge index, exhaust it by finite cases, and discharge each inequality by numeric normalization on the table. Volume positivity: rewrite the Cayley-Menger cubic via the upstream evaluation theorem that sets it equal to $8$, then normalize.
why it matters
This is the local geometric atom for the finite Freudenthal cube triangulation (8 vertices, 19 edges, 6 tets) and for its incidence-consistency witness. Downstream, local-to-global squared-edge agreement theorems identify each tet edge slot with an entry of the global 19-edge table; the same atom is reused for the two-cube strip and the periodic Freudenthal torus. In the Recognition geometry stack it supplies the concrete $D=3$ simplex data that Regge incidence and first-variation bookkeeping sit on top of.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.