firstEndpointVal_edgeBA

Module Crux-2 (Seven Gaps, path-sum) develops quotient bookkeeping for the labeled path-sum measure $Z$. The standing sum is over labeled complexes; the class pushforward rewrites it as a sum over triangulation classes weighted by class mass $|\mathrm{fiber}(q)|\cdot\mu(\mathrm{rep},q)$.

At $B=2$ the fork exhibits two labeled one-edge complexes: one with ordered edge $(0,1)$ and one with ordered edge $(1,0)$. They are related by a vertex-swap relabeling, so they lie in the same quotient class, yet they are distinct as labeled data. The first-endpoint observable reads the numeric first coordinate of edge $0$ (or $0$ if there is no edge) and is the separator used to prove that distinction.

The complex with endpoints $(1,0)$ is the second witness; evaluating the observable on it is the elementary fact recorded here.

One-line term proof by rfl. Unfolding the first-endpoint observable on a complex with nE = 1 selects the first component of edgeVerts ⟨0, _⟩; on the $(1,0)$ witness that component is definitionally the natural number $1$, so the equality holds by reduction.

Feeds directly into the distinctness theorem for the two $B=2$ edge witnesses: if the complexes were equal, congruence on the first-endpoint observable would force $0=1$ after rewriting the two endpoint evaluations. That distinctness is the labeled half of the fork verdict in the module header: the quotient fiber over the edge class is non-singleton, and therefore class mass strictly exceeds the single-complex measure $\mu$.

The detonation is scoped to the labeled path-sum $Z$ of PathSumMeasure (not the exact-shell quotient-sum convention). Within that scope, this one-line evaluation is the numeric pin that makes the inequality of labeled complexes a theorem rather than prose.