pathPlusAutCount
plain-language theorem explainer
Enumerates ordered automorphism candidates for the directed 2-path plus isolated vertex on four labels: pairs of vertex and edge permutations that preserve the fixed incidence map. Downstream Gap2 ratio theorems cite this count (proved equal to 1) against the two-edge count to get the directed inverse-Aut ratio 1/2. The body is a plain Finset filter-and-card definition, not a proof.
Claim. Let $ev$ send the two edge indices to the ordered pairs $(0,1)$ and $(1,2)$ on vertex labels $\{0,1,2,3\}$. Define $\mathrm{pathPlusAutCount}$ as the number of pairs $(\sigma_v,\sigma_e)\in S_4\times S_2$ such that $ev(\sigma_e(e))=(\sigma_v\times\sigma_v)(ev(e))$ for every edge $e$.
background
This module is an uncommitted hostile probe of Gap2 label-erasure (attacks on G1 dependency, definitional collapse, directed Aut recomputation by kernel enumeration, and vacuity). The local census works with two directed edges on four vertex labels, written as an incidence map Fin 2 → Fin 4 × Fin 4.
The witness incidence pathPlusEV is the directed 2-path $0\to 1\to 2$ (one isolated vertex). The Boolean edgeCommOK decides whether a vertex permutation $\sigma_v$ and an edge permutation $\sigma_e$ jointly preserve that incidence: for every edge $e$, the image edge under $\sigma_e$ equals the pair of vertex images under $\sigma_v$. No abstract Aut type appears; candidates are just pairs in $S_4\times S_2$.
The twin definition in Gap2PoissonCoarea carries the same filter-card shape and is documented as "Directed Aut candidates for the path-plus-isolated witness." The two-edge complex has an analogous count used as the other side of the ratio.
proof idea
Definitional, not a proof. Take the finite universe of all pairs $(\sigma_v,\sigma_e)\in\mathrm{Perm}(\mathrm{Fin},4)\times\mathrm{Perm}(\mathrm{Fin},2)$, keep those pairs for which edgeCommOK pathPlusEV returns true, and return the cardinality of the surviving Finset. Evaluation of the count is deferred to pathPlus_autCount_eq_one, which closes by native_decide.
why it matters
Supplies the path-plus side of the directed Aut kernel used throughout Gap2 measure and coarea work. Immediate consumers prove the count equals 1 (pathPlus_autCount_eq_one) and then the inverse-Aut ratio
$({\mathrm{pathPlusAutCount}}):({\mathrm{twoEdgeAutCount}})=1/2$ (autInverseRatio_eq_half, enumerated_mu_ratio_is_half).
That half matches the process-side class-mass ratio at the $(4,2,0)$ census: fibre_ratio_eq_aut_inverse_ratio and c16_process_discrimination package the equality under the named uniformity premise, with Aut appearing only in the comparison theorems. coarea_at_pathPlus rewrites the coarea identity at this witness using the same count.
In the Seven Gaps gravity stack this is the directed correction that replaces the undirected $1/4$ factor; the hostile probe checks that the kernel enumeration does not collapse or vacate under relabeling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.