firstEndpointVal
plain-language theorem explainer
Extracts a single natural number from a bounded complex: the first vertex of edge 0, or 0 if the complex has no edges. Cited as the labeled observable that separates the two B=2 witnesses (edge from 0 to 1 versus edge from 1 to 0). The body is a one-line decidable case split on whether the edge count is positive.
Claim. For a natural bound $B$ and a bounded complex $K$ of size $B$, write $n_E$ for the number of edges of $K$. If $n_E > 0$, let $(v_0,v_1)$ be the ordered pair of vertices of edge index $0$; the first-endpoint value is $v_0$ viewed as a natural number. If $n_E = 0$, the value is $0$.
background
Module Crux-2 of the Seven Gaps gravity stack treats the path-sum partition function $Z$ of labeled bounded complexes and its pushforward onto triangulation classes. The standing sum is over labeled complexes; the quotient by vertex relabeling can have fibers of cardinality greater than one.
A bounded complex $K$ packages a finite edge list edgeVerts indexed by Fin nE. The two B=2 witnesses used in the fork verdict are the single-edge complexes with ordered edge $(0,1)$ and $(1,0)$ respectively. They are related by an explicit vertex-swap relabeling, so they land in the same triangulation class, but they remain distinct as labeled objects.
This definition supplies a concrete numeric probe on the labeled data: the first coordinate of edge 0. It is the observable used to prove those two witnesses are not definitionally equal.
proof idea
Definition, not a proof. On the branch $0 < K.nE$, project the first component of K.edgeVerts at index $0$ (cast to $\mathbb{N}$). On the empty-edge branch, return $0$. No lemmas are invoked.
why it matters
Local parent uses are the two evaluation lemmas (value $0$ on the $(0,1)$ witness, value $1$ on the $(1,0)$ witness) and the inequality theorem that those witnesses are unequal as labeled complexes, proved by congruence of this observable. That inequality is the numeric half of the module's fork verdict: at $B=2$ the class fiber is non-singleton, so class mass equals fiber cardinality times $1/|\mathrm{Aut}|$ and is strictly larger than the bare symmetry factor $\mu$. The detonation is scoped to the labeled path-sum $Z$ only; it does not touch the exact-shell quotient-sum convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.