pathPlusAutCount
plain-language theorem explainer
Counts ordered automorphism candidates of the directed path-plus-isolated complex at census (4,2,0): pairs of vertex and edge permutations that preserve the fixed 2-path incidence. Downstream ratio theorems cite this cardinality as the directed Aut order of that witness. The body is a plain Finset filter over Perm(Fin 4) × Perm(Fin 2).
Claim. Fix the incidence map on four labeled vertices and two directed edges with $e_0 \mapsto (0,1)$ and $e_1 \mapsto (1,2)$ (a directed 2-path plus an isolated vertex). 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 equal to the $\sigma_V$-images of the original endpoints.
background
Gap 2 / A20 (lane C16) studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. At equal census $(4,2,0)$ the stationary class-mass ratio of two Aut-distinct complexes is claimed to be exactly $1/2$ after a directed Aut correction. Process symbols deliberately avoid Aut language; Aut appears only in comparison conclusions.
The witness here is the path-plus-isolated complex: two edges forming a directed path $0\to 1\to 2$ with vertex 3 unused. Its incidence map is the fixed function sending edge $0$ to $(0,1)$ and edge $1$ to $(1,2)$. The Boolean edge-commutation predicate on a pair of permutations $(\sigma_V,\sigma_E)$ holds when every edge is preserved under simultaneous vertex and edge relabeling: $\mathrm{ev}(\sigma_E e)=(\sigma_V\times\sigma_V)(\mathrm{ev}, e)$.
Fibre size equals the sort-respecting arrival count $n_V!,n_E!,n_T!$ divided by directed Aut order (orbit-stabilizer, conclusion side only). This definition supplies that directed order for the path-plus witness.
proof idea
Pure definition, not a proof. Enumerate the finite product $S_4\times S_2$ as a Finset, retain only pairs that satisfy the edge-commutation Boolean on the path-plus incidence map, and take cardinality. No lemmas are applied; evaluation is deferred to later native_decide theorems that pin the count at 1.
why it matters
Supplies the directed Aut numerator for the Gap-2 ratio test. Parent results include: the inverse-Aut ratio equals $1/2$ once the companion two-edge count is 2 and this count is 1; the coarea identity at the path-plus fibre equates factorial-normalized fibre size to the reciprocal of this count; and the process-discrimination package equates the $\pi$-weighted class-mass ratio under uniformity to this Aut-inverse ratio.
In the hostile-probe twin module the same cardinality feeds the enumerated $\mu$-ratio theorem (class-mass ratio $1/2$, not the undirected $1/4$) and the kernel fact that the directed 2-path plus isolated vertex has exactly one ordered Aut candidate. Together these close the directed Aut correction half of the A20 coarea claim at the $(4,2,0)$ witnesses without moving Flag 8 or importing the full theory ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.