twoEdgeEV
plain-language theorem explainer
Names the two-edge witness complex at census (4,2,0): two disjoint directed edges on four vertices, with edge 0 as (0,1) and edge 1 as (2,3). Gravity and Gap-2 coarea arguments cite it as one of the equal-census Aut-distinct pair used for the stationary class-mass ratio test. The definition is a pure lookup table on Fin 2.
Claim. The two-edge endpoint map $e \mapsto (v_0(e), v_1(e))$ on four labelled vertices is $0 \mapsto (0,1)$ and $1 \mapsto (2,3)$. Equivalently, the complex is two disjoint directed edges on the vertex set $\{0,1,2,3\}$.
background
Gap 2 (lane C16) studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. Legal moves (append vertex, unpost unused max vertex, append edge, unpost max edge) each have rate 1. On finite caps the off-diagonal rate matrix is symmetric, so the unique stationary law is uniform on named states.
At equal census $(nV,nE,nT)=(4,2,0)$ two Aut-distinct complexes are compared: the two-edge complex (this map) and the path-plus-isolated complex. Under uniform $\pi$, the $\pi$-weighted class-mass ratio is exactly $1/2$, coming from directed Aut fibre sizes 24 and 48. Process symbols deliberately avoid Aut/orbit language except in conclusions.
twoEdgeEV is the concrete edge-endpoint table for the first witness. It is re-exported from the hostile-probe module into the Poisson-coarea module so Aut enumeration and fibre cardinality can be stated locally.
proof idea
Pure definition: a one-line function on Fin 2 that returns the ordered endpoint pair (0,1) when the edge index is 0 and (2,3) otherwise. No lemmas, tactics, or proof obligations.
why it matters
This table is the carrier for the two-edge side of the Gap-2 ratio test. Downstream, twoEdgeAutCount enumerates directed Aut candidates by filtering permutations of vertices and edges that preserve ordered incidence (edgeCommOK). Companion facts show the identity and the component-swap inhabit that kernel, while ordered edge-flip fails, so the directed Aut order is not the undirected one.
Those counts feed the fibre size and the exact rational ratio $1/2$ under uniform stationary mass (clause $\beta$ of the module headline). The same witness appears in the SJ-tilted decoy receipt that excludes a non-unit $q^{\Delta SJ}$ tilt at these points. Flag 8 and FullTheoryLedger stay untouched; the object is local scaffolding for the Poisson coarea measurement, not a global gravity law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.