tetEdges
plain-language theorem explainer
Enumerates the six edges of a tetrahedron on vertices {0,1,2,3} as ordered pairs with first index strictly smaller. Anyone building the minimal simplicial witness for the path-sum configuration class cites this list. The body is a literal array of the six unordered pairs written in ordered form.
Claim. Define a map $e \colon \{0,\ldots,5\} \to \{0,1,2,3\}^2$ by listing the six edges of $K_4$: $e(0)=(0,1)$, $e(1)=(0,2)$, $e(2)=(0,3)$, $e(3)=(1,2)$, $e(4)=(1,3)$, $e(5)=(2,3)$. Each pair is ordered so the first coordinate is strictly smaller than the second.
background
The module carves the true simplicial subclass out of BoundedComplex, the garbage-inclusive superclass of bounded incidence configurations used by the path-sum measure. A configuration is simplicial when edges are non-degenerate and multi-edge-free, every tetrahedron has four distinct vertices, and the 1-skeleton is closed under every vertex pair of every tetrahedron.
A tetrahedron on four labeled vertices has exactly $\binom{4}{2}=6$ edges. This definition supplies that complete 1-skeleton as an explicit function from edge indices Fin 6 into ordered pairs of vertex indices Fin 4 × Fin 4, always written with the smaller index first. Face (triangle) data is not carried by the ambient configuration type, so only edge and tet incidence appear here.
The list is the combinatorial input needed to exhibit a non-empty simplicial witness rather than relying on the empty complex alone for positivity of the simplicial subclass.
proof idea
Pure data definition: a single array literal of the six ordered pairs. No lemmas, no tactics, no computation. The ordering convention $i<j$ is hard-coded in the list so downstream injectivity and non-degeneracy checks become finite decide goals.
why it matters
Feeds oneTetComplex, the single-tetrahedron complex at the minimal cap (4 vertices, 6 edges, 1 tetrahedron). That witness is what makes simplicialComplex_card_pos non-vacuous: the simplicial subclass is a nonempty Fintype, not merely the empty complex. In the Seven Gaps gravity track this is Phase 0b scaffolding for the path-sum configuration class, ensuring later gap arguments can quantify over genuine abstract simplicial 3-complexes rather than degenerate incidence lists. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is combinatorial infrastructure for the gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.