edgeSwapRelabel
plain-language theorem explainer
Explicit vertex-swap relabeling that identifies the one-edge complex with edge (0,1) with the one-edge complex with edge (1,0) on two vertices. Downstream non-singleton-fiber theorems cite it as the concrete witness that labeled quotient fibers need not be singletons. The construction is a structure instance: swap vertices 0 and 1, leave edges and tetrahedra fixed, and discharge the two commutation fields by swap lemmas and vacuous tet elimination.
Claim. There is an explicit relabeling equivalence between the two labeled one-edge complexes on $B=2$ vertices: the complex whose unique edge is $(0,1)$ and the complex whose unique edge is $(1,0)$. The vertex map is the transposition of the two labels; the edge and tetrahedron maps are the identity; the edge-incidence and tet-incidence diagrams commute.
background
Module Crux-2 (Seven Gaps, path-sum pillar) develops quotient bookkeeping for the labeled path-sum partition function $Z$. Complexes are finite labeled triangulations on a vertex bound $B$; two complexes are equivalent when a Relabel structure supplies vertex/edge/tet bijections that preserve incidence. The quotient by that setoid is TriangulationClass.
The two witnesses at $B=2$ are the one-edge complexes edgeAB (edge $(0,1)$) and edgeBA (edge $(1,0)$). They are distinct as labeled data, yet related by swapping the two vertex labels. Class mass on a quotient class is $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$, not bare $1/|\mathrm{Aut}|$; that distinction is the C1 landmine the module detonates.
Relabel is the structure package for a single equivalence witness: vertex equivalence, edge equivalence, tet equivalence, plus the two commutation identities edge_comm and tet_comm.
proof idea
Structure instance, not a tactic proof. Vertex map is Equiv.swap 0 1 on Fin 2. Edge and tetrahedron maps are Equiv.refl. The edge-commutation field reduces to showing that swapping endpoints of $(0,1)$ yields $(1,0)$, discharged by Equiv.swap_apply_left and Equiv.swap_apply_right. The tet-commutation field is vacuous: there are no tetrahedra on this complex, so t.elim0 closes it.
why it matters
This is the concrete equivalence package inside the T3 fork verdict. exists_nonSingleton_fiber packages it as $\langle\mathrm{edgeAB},\mathrm{edgeBA},\mathrm{ne},\langle\mathrm{edgeSwapRelabel}\rangle\rangle$, proving two distinct labeled complexes lie in one class. one_lt_fiberCard_edgeClass then shows the fiber cardinality of that class is strictly greater than 1.
Together they force the kernel fact that class mass equals $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$ and already differs from a pure $1/|\mathrm{Aut}|$ class sum at $B=2$. Scope is the labeled path-sum $Z$ of PathSumMeasure only; the exact-shell $Z_{\mathrm{RS}}$ uses a different quotient convention and is not contradicted. No forcing-chain landmark (T5–T8) is touched; this is pure combinatorial bookkeeping for the gravity path sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.