pathPlus_autCount_eq_one
plain-language theorem explainer
At census (4,2,0), the directed 2-path plus isolated vertex has exactly one ordered automorphism candidate under vertex/edge relabeling. Anyone computing the Aut-corrected class-mass ratio against the two-edge complex cites this count. The proof is a finite native_decide enumeration of the product of permutation groups.
Claim. The number of ordered pairs $(\sigma_V,\sigma_E)\in S_4\times S_2$ that preserve the directed edge-commutation structure of the path-plus-isolated-vertex incidence equals $1$.
background
Gap 2 / A20 studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. Every legal move has rate 1; on each finite cap the stationary law is uniform. The headline comparison is at equal census $(nV,nE,nT)=(4,2,0)$: the two Aut-distinct witnesses twoEdgeComplex (two disjoint directed edges) and pathPlusIsolated (a directed 2-path plus an isolated vertex).
The quantity pathPlusAutCount is the cardinality of the finite filter of pairs in $S_4\times S_2$ that satisfy the ordered edge-commutation predicate on the path-plus incidence. Process language is firewalled from Aut/orbit vocabulary; Aut counts appear only on the conclusion side of the ratio test. The factorial $nV!,nE!,nT!$ is the count of sort-respecting arrival orders, not an extra hypothesis.
Upstream, the same kernel count is recorded in the label-erasure hostile probe: the directed 2-path plus isolated vertex has exactly one ordered Aut candidate, while two disjoint directed edges have exactly two.
proof idea
One-line computational proof: native_decide exhaustively evaluates the Finset filter defining pathPlusAutCount over the finite type Equiv.Perm (Fin 4) × Equiv.Perm (Fin 2) and checks that exactly one pair satisfies edgeCommOK on the path-plus edge-vertex incidence. No algebraic lemmas are invoked.
why it matters
This unit Aut count is the path-plus half of the directed Aut correction that forces the stationary class-mass ratio at $(4,2,0)$ to be exactly $1/2$, not the undirected $1/4$. Downstream, autInverseRatio_eq_half rewrites the inverse-Aut ratio as $1/2$ from this fact plus twoEdge_autCount_eq_two; enumerated_mu_ratio_is_half does the same for the mu/class-mass form; coarea_at_pathPlus and pathPlus_fibre_eq_orders_div_aut use it to match fibre size to arrival-count divided by Aut order (orbit-stabilizer arithmetic on the conclusion side only).
In the module headline, flag 8 stays unmoved and C23 is explicitly not claimed fully satisfied. The result is a kernel enumeration supporting the Poisson coarea ratio test under the uniformity premise, not a general Aut classification of all tet-free complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.