twoEdgeAutCount
plain-language theorem explainer
Counts ordered automorphism candidates of the two-edge witness graph: two disjoint directed edges on four vertices. The count is the cardinality of permutation pairs (vertex perm on Fin 4, edge perm on Fin 2) that preserve the fixed incidence map under ordered edge-commutation. Downstream theorems evaluate it to 2 and feed the directed inverse-Aut ratio 1/2 used in coarea and class-mass comparisons. Definition is pure kernel enumeration over the finite product of symmetric groups.
Claim. Let the two-edge incidence map send edge $0$ to the ordered pair $(0,1)$ and edge $1$ to $(2,3)$. Define $N$ as the number of pairs $(\sigma_v,\sigma_e)\in S_4\times S_2$ such that for every edge $e$, the image of $e$ under $\sigma_e$ has endpoints exactly $\sigma_v$ applied componentwise to the original endpoints. Then $N\in\mathbb{N}$ is this cardinality.
background
This module is an uncommitted adversarial probe of Gap 2 label-erasure material: it recomputes directed automorphism data by brute-force kernel enumeration rather than by an abstract Aut type. The local objects are small finite complexes on four vertices and two edges.
The incidence witness twoEdgeEV is the map Fin 2 → Fin 4 × Fin 4 with values (0,1) and (2,3): two disjoint directed edges. The Boolean predicate edge-commutation asks whether a vertex permutation σ_v and an edge permutation σ_e jointly preserve that incidence in the ordered sense: for every edge e, the permuted edge's endpoint pair equals (σ_v,σ_v) applied to the original pair. No automorphism group object is constructed; only the Boolean filter on S_4 × S_2 appears.
The same pattern is duplicated in the Poisson-coarea module, where the doc-comment calls this count "Directed Aut candidates for the two-edge witness (kernel enumeration)." Parallel counts exist for the path-plus-isolated witness.
proof idea
Pure definitional card of a filtered Finset. Universe of candidates is Finset.univ on Equiv.Perm (Fin 4) × Equiv.Perm (Fin 2). The filter retains those pairs for which edgeCommOK holds on the fixed two-edge incidence map. The natural number is that filter's cardinality. No lemmas are invoked; evaluation to 2 is deferred to the native_decide theorem twoEdge_autCount_eq_two.
why it matters
Supplies the directed Aut numerator/denominator used throughout Gap 2 measure and coarea arithmetic. Parent results include twoEdge_autCount_eq_two (kernel equals 2), enumerated_mu_ratio_is_half (class-mass/mu ratio 1/2 rather than the undirected 1/4), autInverseRatio_eq_half, fibre_ratio_eq_aut_inverse_ratio, and coarea_at_twoEdge (order-erasure weight times fibre equals inverse directed-Aut order). The process-discrimination package c16_process_discrimination compares the π-weighted class-mass ratio at census (4,2,0) against pathPlusAutCount / twoEdgeAutCount.
In the Recognition gravity stack this is the concrete directed count that replaces undirected Aut bookkeeping when label erasure and Poisson coarea are forced to match. Aut appears only in comparison theorems; the definition itself stays a Boolean kernel on permutation pairs. It closes the hostile-probe attack path D (directed Aut recomputation via kernel enumeration) for the two-edge witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.