pathPlus_autCount_eq_one
plain-language theorem explainer
The directed 2-path plus isolated vertex has exactly one ordered automorphism candidate under the kernel edge-commutation filter. Gravity Gap-2 label-erasure and Poisson-coarea arguments cite this to pin Aut-inverse and class-mass ratios at 1/2 rather than the undirected 1/4. The proof is a one-line native decision over the finite filter on Perm(Fin 4) × Perm(Fin 2).
Claim. The number of ordered automorphism candidates of the directed 2-path with an isolated vertex equals $1$: filtering $\mathrm{Perm}(\mathrm{Fin}\,4)\times\mathrm{Perm}(\mathrm{Fin}\,2)$ by ordered edge-commutation on that incidence yields a singleton.
background
This sits in the hostile-probe module for Gap-2 label erasure (attacks on G1 dependency, directed Aut recomputation by kernel enumeration, and fibre counts). The witness is a four-vertex, two-edge incidence: a directed 2-path plus an isolated vertex. Ordered Aut candidates are pairs of permutations of the four vertices and two directed edges that preserve ordered incidence under the edge-commutation predicate.
The count pathPlusAutCount is the cardinality of that filtered finite set. A sibling count for two disjoint directed edges is two; the ratio of those kernel Aut numbers is the directed analogue of the classical orbit-stabilizer factor. Upstream, the same filter appears in the Poisson-coarea Gap-2 development, where Aut-inverse ratios are compared to fibre ratios of ordered relabelings.
proof idea
Term-mode one-liner: native_decide evaluates the Finset filter defining the Aut-candidate count on Perm(Fin 4) × Perm(Fin 2) against the path-plus incidence and checks that the resulting natural number is 1. No algebraic lemmas are invoked; the claim is pure finite enumeration of the ordered edge-commutation kernel.
why it matters
Feeds the enumerated class-mass / mu ratio theorem in this module, which obtains $1/2$ (not the undirected $1/4$) by rewriting with this fact and the two-edge Aut count equaling 2. Downstream in Gap-2 Poisson coarea it likewise discharges the Aut-inverse ratio equaling $1/2$, the coarea identity at the path-plus fibre, and the fibre-equals-orders-over-Aut arithmetic. Those steps close the directed-Aut side of the label-erasure hostile probe without moving the measure flag. In the broader Seven Gaps gravity stack this is kernel bookkeeping for ordered incidence, not a claim about continuum gravity or the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.