edgeAB_ne_edgeBA
plain-language theorem explainer
The two one-edge labeled complexes at bound B=2, with directed edges (0,1) and (1,0), are unequal as labeled objects. Anyone citing the T3 fork verdict (non-singleton triangulation fibers) needs this separation. The proof is a one-step contradiction on the first-endpoint observable, discharged by norm_num.
Claim. At bound $B=2$, the labeled complex with single edge $(0,1)$ is not equal to the labeled complex with single edge $(1,0)$. They differ as labeled data (their first-endpoint observables disagree).
background
Module Crux-2 (Seven Gaps, path-sum pillar) treats the class pushforward of the labeled path-sum partition function $Z$. Complexes are taken up to vertex relabeling; the quotient is TriangulationClass. Class mass is defined fiberwise: $\mathrm{classMass}(q)=|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep},q)|)$, not the bare $1/|\mathrm{Aut}|$ weight.
The two witnesses are the minimal one-edge complexes at $B=2$: one carries the ordered edge $(0,1)$, the other $(1,0)$. Equivalence under the vertex-swap relabeling is separate; this lemma only asserts they are distinct as labeled complexes. Distinction is read off the labeled observable that records the first endpoint value of the unique edge.
Upstream bookkeeping (sum_fiberwise_quotient, classMass_eq_fiberCard_mul_mu) already decomposes $Z$ over quotient fibers. The present inequality is the kernel fact that those fibers need not be singletons.
proof idea
Term-mode proof by contradiction. Assume the two labeled complexes are equal. Apply congruence of the first-endpoint valuation to that equality, then rewrite with the two evaluation lemmas for each witness. The resulting numeric equality is absurd by norm_num. No quotient or automorphism facts are used; only the labeled observable separates them.
why it matters
Feeds the T3 fork verdict directly. Downstream, exists_nonSingleton_fiber packages the pair as an explicit witness of two distinct yet equivalent labeled complexes at $B=2$, and one_lt_fiberCard_edgeClass upgrades that to fiber cardinality strictly greater than one. Together they detonate the C1 landmine: labeled pushforward mass genuinely carries the $|\mathrm{fiber}|$ factor and differs from a pure inequivalent-class $1/|\mathrm{Aut}|$ sum already at the smallest nontrivial bound.
Scope of the detonation is the labeled path-sum $Z$ of PathSumMeasure only; the exact-shell $Z_{RS}$ wave uses a different (quotient-sum) convention and is not contradicted. In the Seven Gaps gravity stack this locks the honest measure bookkeeping before any continuum or phenomenological claim is drawn from class-averaged weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.