localEdgeOf
plain-language theorem explainer
Lookup table sending each of the twelve tetrahedra and each of its six local edge slots to one of the thirty-three global edges of the two-cube Freudenthal strip. Anyone proving multi-cube edge-slot partitions or incidence consistency cites this table. It is pure exhaustive case data: no proof body, just the chosen global representatives.
Claim. For every tetrahedron $\tau\in\{0,\ldots,11\}$ and every local edge slot $f\in\{0,\ldots,5\}$, assign a global edge index $e\in\{0,\ldots,32\}$ that represents that local tetrahedral edge in the two-cube Freudenthal strip (two unit cubes sharing a face, twelve tets, thirty-three unique edges after shared-face deduplication).
background
The two-cube Freudenthal strip is the smallest nontrivial multi-cube example in this geometry stack: two unit cubes glued along one square face, each decomposed into six Freudenthal tetrahedra with matching face triangulation. The module indexes twelve tetrahedra and thirty-three unique global edges (five shared-face edges are not double-counted).
Each Freudenthal tetrahedron carries six edges. The single-cube precursor already fixes, for each of six tets and six slots, a global edge among the nineteen cube edges. The present map extends that assignment across both cubes, reusing the shared-face edge indices where the cubes meet.
Local theoretical setting is combinatorial incidence only: vertices, edges, tets, and slot-to-edge tables that later feed partition and consistency lemmas.
proof idea
Definition by exhaustive pattern match on tetrahedron index (twelve cases) and local slot (six cases). Each clause is a constant global edge index in ${0,\ldots,32}$. There is no proof body and no tactic script; the table is the content.
Downstream inverse-lookup lemmas recover the slot from a global edge by comparing against these twelve-by-six values, typically discharged by a decision procedure on finite types.
why it matters
This table is the incidence witness for the two-cube strip. It is consumed by the edge-in-tetrahedron membership test, the iff relating membership to the table, local-edge completeness, and the global local-edge-slot partition after shared-face deduplication.
The module presents this strip as the first concrete multi-cube incidence instance beyond the one-cube sanity check. The same pattern reappears, translated by cell offsets, in the periodic Freudenthal torus construction. In the broader Recognition geometry stack these discrete cube-and-tet complexes support lattice incidence used toward spatial $D=3$ and eight-tick discrete structure, though this declaration itself is pure finite combinatorics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.