exists_nonSingleton_fiber
plain-language theorem explainer
At bound B=2 there are two distinct labeled complexes in the same triangulation class: the one-edge complexes with directed edges (0,1) and (1,0). Anyone decomposing the labeled path-sum Z over TriangulationClass cites this as the C1 fork verdict: quotient fibers are not all singletons. The proof is a pure term witness pairing those two edges via an explicit vertex-swap relabeling.
Claim. There exist two distinct labeled complexes $K,K'$ of bound $B=2$ that are equivalent under vertex relabeling: $K\neq K'$ and $K\sim K'$. Explicitly, the one-edge complex with edge $(0,1)$ and the one-edge complex with edge $(1,0)$ form such a pair.
background
The module treats Crux-2 of the Seven Gaps program: the class pushforward of the labeled path-sum partition function $Z$. Protocol is quotient bookkeeping. Complexes are labeled; the setoid Equivalent identifies those related by vertex relabeling, and TriangulationClass B is the quotient.
For a class $q$, the pushforward mass is defined by summing the labeled measure $\mu$ over the fiber: $\mathrm{classMass}(q)=\sum_{K:\llbracket K\rrbracket=q}\mu(K)$. By the sibling identity this equals $|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep},q)|)$, not the bare $1/|\mathrm{Aut}|$ weight. Whether fibers can have cardinality greater than one is therefore a kernel fact, not a convention.
The standing $Z$ of PathSumMeasure is the labeled sum. The exact-shell $Z_{\mathrm{RS},uv}$ uses a different (quotient-sum) convention; the two are not identified here.
proof idea
Pure term-mode existence proof. The two witnesses are the named one-edge complexes edgeAB (edge $(0,1)$) and edgeBA (edge $(1,0)$) at $B=2$. Distinctness is the lemma edgeAB_ne_edgeBA. Equivalence is packaged as ⟨edgeSwapRelabel⟩, the explicit vertex-swap relabeling that swaps the two endpoints and carries one complex to the other. No tactics, no search: four constructors assembled into an existential pair.
why it matters
This is the T3 fork verdict that detonates the C1 landmine as a kernel fact: quotient fibers of TriangulationClass are not all singletons, so labeled pushforward mass genuinely differs from per-class $1/|\mathrm{Aut}|$ weights. Downstream, does records that $Z$ is not the inequivalent-class sum with weights $1/|\mathrm{Aut}|$, and the numeric separation μ(edgeAB)<\mathrm{classMass}(⟦edgeAB⟧) is built on this witness (via the count-form sibling that the edge-class fiber has cardinality $>1$).
In the Seven Gaps / path-sum pillar this locks the bookkeeping convention for the labeled $Z$: every later class decomposition must carry the factor $|\mathrm{fiber}|$. Scope of the detonation is only that labeled sum; it does not touch the exact-shell gauge wave, which is defined in the quotient-sum convention by its own header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.