twoEdgeEV
plain-language theorem explainer
Defines the two-edge witness incidence map: two directed edges on four vertices, sending edge 0 to (0,1) and edge 1 to (2,3). Hostile-probe and Poisson-coarea modules cite it as the carrier for directed Aut enumeration and edge-commutation checks. The body is a one-line piecewise constant function on Fin 2.
Claim. The two-edge incidence map $E\colon \{0,1\}\to \{0,1,2,3\}\times\{0,1,2,3\}$ is given by $E(0)=(0,1)$ and $E(1)=(2,3)$: two disjoint directed edges on a four-vertex carrier.
background
The module is an uncommitted adversarial probe of Gap2 label-erasure claims (G1 dependency, directed Aut recomputation, fibre counts). It reuses the same two-edge witness already present in Gap2PoissonCoarea.
Here an incidence map assigns to each abstract edge a directed ordered pair of vertices. The two-edge map places edge 0 on the ordered pair $(0,1)$ and edge 1 on $(2,3)$, so the underlying complex is two disjoint directed edges on $\mathrm{Fin},4$. Downstream filters test which pairs of vertex and edge permutations preserve this ordered incidence (the edgeCommOK predicate).
The same definition appears upstream in Gap2PoissonCoarea as the carrier for kernel enumeration of directed Aut candidates.
proof idea
Pure definitional abbreviation: a single fun with an if e = 0 branch returning the ordered pairs $(0,1)$ and $(2,3)$. No lemmas, no tactics.
why it matters
Supplies the concrete directed carrier on which the hostile probe enumerates Aut candidates and checks ordered edge-commutation. Downstream, twoEdgeAutCount counts permutations $p$ with edgeCommOK twoEdgeEV p.1 p.2; the native-decide theorems twoEdge_id_ok, twoEdge_component_swap_ok, and twoEdge_edge_flip_fails_comm show that identity and component swap preserve incidence while edge reversal does not. That directed-vs-undirected distinction feeds the class-mass / $\mu$ ratio claim (enumerated factor $1/2$, not the undirected $1/4$) inside the Gap2 label-erasure and Poisson-coarea stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.