freudenthalCube_incidenceConsistent
plain-language theorem explainer
Packages incidence consistency for the standard Freudenthal split of the unit cube into six tetrahedra along the body diagonal. Discrete-geometry and Regge-calculus workers cite it when they need a verified incidence interface on this mesh. The body is a structure instance: each field is discharged by a prior local lemma (vertex matching, length agreement, edge completeness, Schläfli closed form).
Claim. The Freudenthal six-tetrahedron triangulation of the unit cube is incidence-consistent: a global squared-length assignment on its $19$ edges is fixed; whenever a global edge appears in a tetrahedron, its endpoints match that tetrahedron's local edge vertices (up to order); local squared lengths equal the global ones; every local edge slot of every tetrahedron is realized by some global edge; and each tetrahedron satisfies the closed-form Schläfli identity.
background
This module builds the standard Freudenthal decomposition of one unit cube into six tetrahedra, using the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Cube vertices are labeled by binary coordinates; the six tets are the monotone lattice paths from $0$ to $7$. The finite triangulation record has $8$ vertices, $19$ edges, and $6$ tets, with explicit edge- and tet-vertex tables.
Incidence consistency is the interface that ties global edge data to local tet data: a global squared-length map, a proof that edges inside a tet hit the correct local vertices, agreement of local and global squared lengths, surjectivity of the local-edge map onto each tet's six slots, and a local Schläfli identity per tet. Upstream, a nondegenerate unit Freudenthal tet supplies the closed-form Schläfli input; separate lemmas already prove vertex matching, local-to-global length equality, and completeness of local edges.
proof idea
Structure-instance construction for the incidence-consistency interface on the Freudenthal cube triangulation. The global squared-length field is the precomputed map on the $19$ edges. The four proof fields are one-line wrappers: vertex matching applies the prior edge-in-tet vertices theorem; length agreement applies the local-equals-global squared-edge lemma; completeness applies the local-edge completeness theorem (via the local-edge-of map and its iff); the local Schläfli field applies the closed-form Schläfli identity to the nondegenerate unit Freudenthal tetrahedron.
why it matters
This is the incidence package that the Freudenthal cube needs before any edge-slot bookkeeping. Downstream, the unique/no-duplication local edge-slot partition is built on top of it, and the concrete edge-slot bookkeeping instance is obtained from that partition. Together they turn the six-tet cube into a mesh whose first-variation and Regge-action arguments can quote a single verified incidence object rather than ad-hoc edge tables.
In the broader Recognition geometry stack this is scaffolding for discrete curvature and action on the cube, not a forcing-chain step (T0–T8). It closes the incidence side of the Freudenthal cube so later variation lemmas can treat edges and tets uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.