edgeInTet_iff_localEdgeOf
plain-language theorem explainer
On the Freudenthal six-tetrahedron unit cube, a global edge sits in a given local edge slot of a tetrahedron exactly when it is the designated representative of that slot. Incidence and partition lemmas for the cube (and the two-cube strip) cite this equivalence. The proof is exhaustive finite case analysis of the lookup tables.
Claim. For every global edge index $e\in\{0,\ldots,18\}$, tetrahedron $\tau\in\{0,\ldots,5\}$, and local edge slot $f\in\{0,\ldots,5\}$, the incidence map returns $\mathrm{some}\,f$ on tetrahedron $\tau$ for edge $e$ if and only if $e$ equals the designated global representative of slot $f$ on $\tau$.
background
The module fixes the standard Freudenthal decomposition of the 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 $0..7$; the six tets are the monotone paths from $0$ to $7$.
Global edges are indexed by $\mathrm{Fin},19$. Each tetrahedron has six local edge slots ($\mathrm{Fin},6$). The map localEdgeOf chooses, for each tet and local slot, one global edge representative. The map edgeInTet is the inverse-looking incidence: given a global edge and a tet, it returns the local slot if that edge belongs to the tet, else none.
The same incidence pattern appears in the two-cube strip and (translated) on the periodic Freudenthal torus; those modules reuse or mirror this cube-level bookkeeping.
proof idea
Pure finite enumeration. Case-split on the three finite indices (global edge, tetrahedron, local slot), then simplify both sides against the explicit pattern-matching definitions of the incidence map and the local-to-global representative. No algebraic lemma is needed beyond unfolding the two lookup tables; every cell of the $19\times 6\times 6$ table is checked directly.
why it matters
This biconditional is the hinge between the two incidence tables. Downstream, freudenthalCube_edgeSlotPartition installs it as the edgeInTet_iff field of the incidence edge-slot partition instance, asserting unique/no-duplication local slots on the cube. localEdge_complete is a one-line existence corollary: every local slot is hit by its designated global edge.
The two-cube strip reuses the same shape for its own partition, completeness, vertex-consistency, and squared-edge identification lemmas. In the broader RS geometry stack this is discrete incidence hygiene for Regge-style first-variation bookkeeping on Freudenthal triangulations, not a continuum or curvature statement. It does not itself touch T0–T8 or the J-cost; it supplies the combinatorial substrate those continuum limits sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.