sameUnorderedPair4
plain-language theorem explainer
Two ordered endpoint pairs on Fin n are the same undirected edge when they agree or one is the swap of the other. The 4D Freudenthal carrier uses this local predicate (mirroring the 3D path-sum version) to state no-multiedges and skeleton closure. The body is the two-clause disjunction p = q ∨ p = q.swap.
Claim. For $n \in \mathbb{N}$ and ordered pairs $p,q \in \mathrm{Fin}\,n \times \mathrm{Fin}\,n$, declare that $p$ and $q$ represent the same unordered pair when $p = q$ or $p = q^{\mathrm{swap}}$ (the two components exchanged).
background
The module builds the typed periodic Freudenthal triangulation of the 4-torus: four-coordinate periodic vertices, the fifteen positive-displacement edge classes of the 4-cube, and the Kuhn triangulation into $4! = 24$ four-simplices. It is deliberately self-contained because the 3D path-sum carrier BoundedComplex is tetrahedron-only and cannot hold Kuhn 4-simplices with Fin 5 corners.
Edges of a 4D carrier are stored as ordered pairs of vertex indices. Geometric identity of an undirected edge must ignore orientation, so one needs a relation that identifies $(u,v)$ with $(v,u)$. This definition is the local 4D mirror of the 3D sameUnorderedPair from the SevenGaps path-sum layer.
The carrier type records edgeVerts : Fin nE → Fin nV × Fin nV and simplexVerts : Fin nS → Fin 5 → Fin nV. Simpliciality then packages non-degeneracy, uniqueness of undirected edges, injective simplex corners, and skeleton closure in terms of this relation.
proof idea
Pure definition: the proposition is the disjunction that the two ordered pairs are equal, or the first equals the componentwise swap of the second. No lemmas are invoked; downstream proofs case-split on the two arms or rewrite with Prod.swap.
why it matters
This predicate is the undirected-edge equality used by the 4D simplicial interface. IsSimplicial4D requires that equal unordered endpoint pairs force equal edge indices (no multi-edges) and that every distinct corner pair of every 4-simplex appears as some carrier edge (skeleton closure).
Those clauses are discharged for the canonical carrier by canonicalCarrier4D_no_multiedges and canonicalCarrier4D_skeleton. Together they make the Kuhn 4-torus mesh a genuine simplicial complex in the module's self-contained Carrier4D shape, which the 4D MetricRefinementFamily reconstruction named as the missing geometric object. The definition does not itself touch T0–T8 or the RCL; it is combinatorial scaffolding for the 4D geometry layer that will feed that assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.