edgeInTet_iff_localEdgeOf
plain-language theorem explainer
The incidence map sending a global edge and tetrahedron to a local edge slot returns some f exactly when that edge is the designated local edge of the tetrahedron at slot f. Combinatorial geometers of the two-cube Freudenthal strip cite this to convert incidence queries into the explicit local-edge table (and back). The proof is a one-line native_decide on the finite index types Fin 33, Fin 12, and Fin 6.
Claim. For every global edge $e\in\{0,\ldots,32\}$, every tetrahedron $\tau\in\{0,\ldots,11\}$, and every local edge slot $f\in\{0,\ldots,5\}$, the incidence map returns $\mathrm{some}\,f$ if and only if $e$ equals the designated global edge of tetrahedron $\tau$ at slot $f$.
background
The two-cube Freudenthal strip is the smallest nontrivial multi-cube example: two unit cubes sharing one square face, each cut into six Freudenthal tetrahedra with compatible face triangulation. After deduplicating the five shared-face edges one obtains 33 global edges (indexed by Fin 33) and 12 tetrahedra (indexed by Fin 12).
The incidence map records whether a global edge belongs to a given tetrahedron and, if so, which of its six local edge slots it occupies. The companion table picks, for each tetrahedron and slot, the unique global edge filling that slot. The one-cube module already proves the same biconditional on 19 edges and 6 tets; this is the strip-scale analogue needed once shared-face edges are identified.
proof idea
One-line wrapper: native_decide +replace exhaustively decides the finite biconditional over all triples from Fin 33, Fin 12, and Fin 6. No algebraic lemmas are called; the decision procedure evaluates the lookup tables that define the incidence map and the local-edge table on every input.
why it matters
This biconditional is the conversion lemma that turns the explicit local-edge table into an incidence relation the partition machinery can use. Downstream it discharges the incidence field of the two-cube edge-slot partition, powers completeness (every local slot is occupied), square-edge label agreement with the global table, and endpoint consistency of incident edges. It is the first multi-cube incidence instance beyond the single-cube sanity check, and the parallel of the one-cube edge-slot partition that feeds the discrete geometry layer used by later Freudenthal and Regge-style constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.