twoEdge_autCount_eq_two
plain-language theorem explainer
Two disjoint directed edges on four named vertices admit exactly two ordered automorphism candidates. Gravity and coarea arguments that correct class mass by directed Aut order at the equal-census pair (4,2,0) cite this count. The proof is a one-line native decision over the finite set of vertex/edge permutation pairs that preserve incidence.
Claim. The number of ordered pairs $(\sigma_V,\sigma_E)\in S_4\times S_2$ that preserve the directed edge-incidence relation of the two-edge witness complex equals $2$.
background
Gap 2 (A20, lane C16) studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. Legal moves (append vertex, unpost max unused vertex, append edge, unpost max edge) each have rate 1. On each finite cap 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 witnesses are compared: the two-edge complex (two disjoint directed edges) and the path-plus-isolated complex. Class-mass ratios under uniform $\pi$ reduce to fibre sizes, and fibre size equals the sort-respecting arrival count $nV!,nE!,nT!$ divided by directed Aut order (orbit-stabilizer, conclusion side only).
Directed Aut candidates are enumerated as the cardinality of pairs in $S_4\times S_2$ that commute with the fixed edge-vertex incidence of the witness. The same kernel definition appears in the hostile-probe module; the present module re-exports it for the coarea lane.
proof idea
One-line wrapper: native_decide evaluates the finite filter
Finset.univ.filter (fun p => edgeCommOK twoEdgeEV p.1 p.2)
over $S_4\times S_2$ and checks that its cardinality is exactly 2. No algebraic lemmas are invoked; the decision procedure exhausts the $24\cdot 2=48$ candidate pairs.
why it matters
This count is the directed-Aut denominator for the two-edge witness. Downstream it discharges autInverseRatio_eq_half (path-plus Aut count over two-edge Aut count equals $1/2$), the fibre identity twoEdge_fibre_eq_orders_div_aut, and the scoped coarea identity coarea_at_twoEdge:
order-erasure weight times named fibre $=1/\mathrm{Aut}$.
The hostile-probe twin uses the same fact to prove enumerated_mu_ratio_is_half: the $\mu$-ratio is $1/2$, not the undirected $1/4$. Together these pin the headline that at census $(4,2,0)$ the stationary class-mass ratio of the two Aut-distinct complexes is exactly $1/2$ under uniform $\pi$, with Aut appearing only on the conclusion side. Flag 8 and C23 remain unmoved; the result is witness-local.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.