sameUnorderedPair
plain-language theorem explainer
Two ordered vertex pairs represent the same undirected edge when they are equal or swaps of each other. Gravity and combinatorial-geometry proofs cite this when enforcing that a bounded incidence list has no multi-edges. The body is a one-line disjunction; decidability is inferred from equality and swap on finite indices.
Claim. For ordered pairs $p,q\in\{0,\ldots,n-1\}^{2}$, the unordered-pair relation holds iff $p=q$ or $p=(q_{2},q_{1})$.
background
Phase 0b of the SevenGaps gravity stack carves the true simplicial subclass out of BoundedComplex B, the garbage-inclusive class of bounded incidence configurations (vertex/edge/tet lists). That superclass admits degenerate edges, multi-edges, repeated tet corners, and tets whose 1-skeleton is missing from the edge list.
The simplicial predicate needs a notion of edge identity that ignores orientation: two ordered endpoint pairs count as one undirected edge when they agree or are swaps. This definition supplies that relation on Fin n × Fin n.
The ambient setting is abstract simplicial 3-complexes presented by tetrahedra and 1-skeleton only; face (triangle) data is not carried, so triangle closure is out of scope here.
proof idea
Pure definition: the proposition is the disjunction of equality of the ordered pairs and equality after swapping the second pair's components. A separate Decidable instance unfolds the definition and lets Lean infer decidability from decidable equality on finite products.
why it matters
Feeds the multi-edge clause of the simplicial predicate: for every pair of edge indices, if their endpoint pairs satisfy this relation then the indices coincide. That clause, with no-degenerate-edges, injective tet corners, and skeleton closure, defines the simplicial subclass used to prove the subclass is a nonempty Fintype (via the explicit one-tetrahedron witness).
In the Recognition gravity path-sum measure, only these simplicial configurations are the intended combinatorial triangulations; this helper is the orientation-blind edge equality those checks rest on. It does not itself touch T0–T8 or the mass ladder; it is local combinatorial scaffolding for the gravity configuration class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.