twoEdgeComplex_counts
plain-language theorem explainer
The two-edge complex (two disjoint directed edges on four vertices) has census observables vertex count 4, edge count 2, and tet count 0. Gap-2 / label-erasure auditors cite it as a minimal non-path test complex for fibre and Aut probes. The proof is pure definitional reflexivity on the structure fields.
Claim. For the two-edge complex of two disjoint directed edges $0\to 1$ and $2\to 3$, the vertex count equals $4$, the edge count equals $2$, and the tet (free-label) count equals $0$.
background
The ambient module is an uncommitted hostile probe against Gap-2 label erasure: it stress-tests G1 dependency, definitional collapse, directed Aut recomputation, and vacuity. Census observables live on ensembles: vertex count $n_V$, edge count $n_E$, and tet count $n_T$ (the free label) extract the corresponding real coordinates from a bounded complex.
The two-edge complex is the BoundedComplex 4 with fields fixed at $n_V=4$, $n_E=2$, $n_T=0$, geometrically two disjoint directed edges $0\to 1$ and $2\to 3$. It sits beside the path-plus-isolated complex as a second elementary test shape for incidence and orbit-stabilizer checks in the Gap-2 stack.
proof idea
Term-mode proof: the three conjuncts are definitional equalities of the structure fields of the two-edge complex, discharged by three rfls packaged as an anonymous constructor. No lemmas are invoked.
why it matters
Supplies the census triple for the two-edge test complex inside the Gap-2 label-erasure hostile-probe suite (attacks on G1, directed Aut, fibre counts, and vacuity). No downstream consumers are wired yet; siblings include the analogous path-plus-isolated count lemma and edge-commutation / EV checks. It anchors a minimal disconnected complex so Aut and fibre probes are not path-shaped only. Framework landmarks (T0–T8, RCL, $\phi$-ladder) are not directly invoked; the lemma is pure combinatorial scaffolding for gravity Gap-2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.