edgeAB
plain-language theorem explainer
Canonical two-vertex, one-edge labeled complex at bound B=2 with ordered edge (0,1). It is the first witness in the Crux-2 fork that quotient fibers of labeled triangulations need not be singletons. Defined as an abbrev so size fields reduce under numeral elaboration; inequalities are reflexivity and standard Nat bounds.
Claim. Let $\mathrm{edgeAB}$ be the labeled bounded complex at $B=2$ with $n_V=2$ vertices, $n_E=1$ edge, $n_T=0$ tetrahedra, edge map sending the unique edge to the ordered pair $(0,1)$, and empty tetrahedron map. The bound inequalities $2\le 2$, $1\le 2$, and $0\le 2$ hold.
background
Module Crux-2 (Seven Gaps, pillar 2) treats the class pushforward of the labeled path-sum $Z$. Protocol is QUOTIENT_BOOKKEEPING: sums over labeled complexes decompose over fibers of the relabeling quotient, and class mass is $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$, not bare $1/|\mathrm{Aut}|$ per class.
A BoundedComplex B packages finite vertex/edge/tet counts bounded by $B$, plus maps naming the vertices of each edge and tet. Here $B=2$ is the smallest nontrivial bound: two labels and one directed edge.
The companion complex with edge $(1,0)$ and the explicit swap relabeling live beside this definition. Together they feed the T3 fork verdict that fibers need not be singletons already at $B=2$.
proof idea
Definitional abbrev, not a proved theorem. Fields are filled by numerals and standard inequalities: le_refl 2 for the vertex bound, one_le_two for the edge bound, Nat.zero_le 2 for the tet bound. The unique edge is constantly $(0,1)$; the tet map is elim0 on the empty type Fin 0. Abbrev (vs def) keeps nV, nE, nT reducible during numeral elaboration downstream.
why it matters
Primary witness for the C1 landmine detonation in this module. Downstream, edgeAB_ne_edgeBA separates it from edgeBA via firstEndpointVal; edgeSwapRelabel exhibits an equivalence; exists_nonSingleton_fiber packages the pair as a non-singleton fiber; one_lt_fiberCard_edgeClass and mu_lt_classMass_edgeClass turn that into the numeric fact $\mu(\mathrm{edgeAB}) < \mathrm{classMass}([\mathrm{edgeAB}])$.
That kernel inequality shows the labeled path-sum $Z$ of PathSumMeasure carries fiber-multiplied class mass, distinct from a pure per-class $1/|\mathrm{Aut}|$ sum, already at $B=2$. Scope is the labeled $Z$ only; it does not touch the exact-shell $Z_{RS}$ quotient convention. Also referenced from quotientFirstStatus_grounded in QuotientFirstZ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.