edgeBA
plain-language theorem explainer
Defines the one-edge labeled complex at bound 2 whose single edge runs (1,0), the vertex-order swap of the companion complex with edge (0,1). Downstream fork theorems cite it as the second witness that a triangulation class fiber can have cardinality greater than one. The body is a pure structure literal: size bounds by reflexivity and zero-lemmas, edge map constantly (1,0), empty tet map.
Claim. Let $K_{BA}$ be the bounded labeled complex at $B=2$ with two vertices, one edge, and no tetrahedra, whose unique edge has ordered endpoints $(1,0)$. (Size inequalities hold by reflexivity and $0\le 2$; the tetrahedron map is vacuous.)
background
Module SevenGaps.ClassPushforward carries Crux-2 of the path-sum pillar: quotient bookkeeping for the labeled path-sum $Z$. The standing sum is over labeled complexes; classes are orbits under vertex relabeling. The module proves that when a weight is constant on classes, $Z$ factors as a sum of class masses times the weight on a representative, with $\mathrm{classMass}(q)=|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}|)$, not merely $1/|\mathrm{Aut}|$.
A BoundedComplex B packages finite vertex/edge/tet counts (each at most $B$), the edge endpoint map, and the tet vertex map, plus the three size inequalities. The companion complex with edge $(0,1)$ is the other labeled one-edge object at $B=2$. The present definition is that same skeleton with endpoints swapped to $(1,0)$.
Upstream size lemmas are ordinary order facts (le_refl, zero_le / Nat.zero_le). Geometry modules supply analogous edgeVerts/tetVerts tables for Freudenthal triangulations; here those names are only the structure fields, filled by a constant pair and an empty elim.
proof idea
Definitional abbrev, not a proved theorem. The structure is filled fieldwise: nV=2, nE=1, nT=0; the three inequalities are le_refl 2, one_le_two, and Nat.zero_le 2; edgeVerts ignores its index and returns the ordered pair $(1,0)$; tetVerts is Fin 0-elimination. Marked abbrev so the numeric size fields reduce under numeral elaboration in later proofs.
why it matters
This is the second explicit witness in the T3 fork verdict that triangulation-class fibers need not be singletons. Together with the $(0,1)$ companion it feeds edgeAB_ne_edgeBA (distinctness via the first-endpoint observable), the vertex-swap Relabel equivalence, exists_nonSingleton_fiber, firstEndpointVal_edgeBA, and one_lt_fiberCard_edgeClass.
Those results detonate the C1 landmine as a kernel fact: at $B=2$ already, labeled class mass equals $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$ and is strictly larger than the bare symmetry weight $\mu$ of a single representative. Scope is the labeled path-sum $Z$ of PathSumMeasure only; the exact-shell $Z_{RS}$ quotient convention is a different bookkeeping choice, not a contradiction. In the Seven Gaps gravity stack this locks the correct pushforward weight before any continuum or phenomenological identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.