edgeInTet
plain-language theorem explainer
Incidence query on the two-cube Freudenthal strip: given one of the 33 global edges and one of the 12 tetrahedra, return the local edge slot in {0,...,5} if that edge belongs to the tetrahedron, otherwise none. Cited by anyone checking multi-cube edge-slot partitions or shared-face compatibility. Defined by six equality tests against the tetrahedron's local-edge representatives.
Claim. For a global edge $e$ among the $33$ edges of the two-cube strip and a tetrahedron $\tau$ among the $12$ Freudenthal tetrahedra, return $\mathrm{some}\,f$ with $f\in\{0,\ldots,5\}$ if $e$ equals the global representative of local slot $f$ on $\tau$, and $\mathrm{none}$ otherwise.
background
The two-cube Freudenthal strip is the smallest nontrivial multi-cube example: two unit cubes sharing one square face, each decomposed into six Freudenthal tetrahedra with compatible face triangulation. After deduplicating the five shared-face edges one obtains $33$ global edges (indexed by $\mathrm{Fin},33$) and $12$ tetrahedra (indexed by $\mathrm{Fin},12$).
The companion map localEdgeOf sends each tetrahedron and each of its six local edge slots to a unique global edge index. The one-cube precursor in FreudenthalCubeTriangulation uses the same pattern on $19$ edges and $6$ tetrahedra; its incidence map is documented as "Incidence map from a global edge and tetrahedron to the local edge slot, if the edge belongs to that tetrahedron."
The present definition inverts that assignment into a lookup: edge and tetrahedron in, optional local slot out.
proof idea
Pure definition by cascading equality tests. Compare the input edge against localEdgeOf τ 0, then localEdgeOf τ 1, ..., localEdgeOf τ 5; on the first match return some k, otherwise none. No lemmas are applied; the body is the decision tree itself.
why it matters
This incidence map is the combinatorial backbone of the two-cube strip. Downstream it feeds edgeInTet_iff_localEdgeOf (the equivalence with the local-edge assignment), edgeInTet_vertices (vertex-endpoint consistency of an incident edge), and the global local-edge-slot partition after shared-face deduplication. That partition is the module's main deliverable: the first concrete multi-cube incidence instance beyond the one-cube sanity check.
In the broader Recognition geometry stack the same pattern appears in the single-cube triangulation (freudenthalCube, localEdge_complete, local_sqEdge_eq_global). Those objects supply discrete 3-complex data (edge lengths, tetrahedral incidence) used by Regge-style discrete gravity and lattice constructions consistent with the forced spatial dimension $D=3$ (forcing step T8). The definition itself is scaffolding, not a forcing-chain landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.