twoEdgeAutCount
plain-language theorem explainer
Counts directed automorphisms of the two-edge witness complex at census (4,2,0): pairs of vertex and edge permutations that preserve the directed incidence of two disjoint edges. Gravity Gap-2 / C16 coarea and class-mass ratio proofs cite it as the Aut-order denominator. The body is a finite filter-and-card over Perm(Fin 4) × Perm(Fin 2).
Claim. Define the directed automorphism count of the two-edge witness as the number of pairs $(\sigma_V, \sigma_E) \in S_4 \times S_2$ such that the edge-endpoint map of two disjoint directed edges is equivariant: for every edge $e$, $\mathrm{ev}(\sigma_E e) = (\sigma_V \times \sigma_V)(\mathrm{ev}(e))$.
background
Gap 2 / A20 (lane C16) studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. At equal census $(4,2,0)$ one compares two Aut-distinct named complexes: the two-edge witness (two disjoint directed edges) and the path-plus-isolated witness. Under uniform stationary measure the $\pi$-weighted class-mass ratio is claimed to be exactly $1/2$, matching the directed inverse-Aut ratio.
Process symbols are firewalled away from Aut/orbit language; Aut appears only in conclusions and pre-registered ratio comparisons. The predicate edgeCommOK checks that a candidate pair $(\sigma_V,\sigma_E)$ intertwines the fixed edge-vertex incidence twoEdgeEV: every permuted edge has endpoints equal to the vertex-permuted original endpoints. The factorial $n_V! n_E! n_T!$ counts sort-respecting arrival orders; fibre size is that count divided by directed Aut order (orbit-stabilizer on the conclusion side only).
proof idea
Pure definition: take the finite product universe $S_4 \times S_2$, filter by the Boolean decision of incidence-equivariance for the two-edge endpoint map, and return the cardinality. No lemmas are applied at the definition site; downstream native_decide proofs evaluate the card to 2.
why it matters
Supplies the Aut-order numerator/denominator for the directed correction that turns undirected $1/4$ intuition into the measured ratio $1/2$. Downstream, twoEdge_autCount_eq_two evaluates it to 2; autInverseRatio_eq_half and enumerated_mu_ratio_is_half obtain $(\mathrm{pathPlusAutCount})/(\mathrm{twoEdgeAutCount}) = 1/2$; coarea_at_twoEdge equates order-erasure weight times fibre card to the inverse directed Aut order; c16_process_discrimination packages the process-side discrimination under the uniformity premise. This is the kernel enumeration step of the Poisson recognition coarea argument at the $(4,2,0)$ witnesses, with Flag 8 unmoved and no FullTheoryLedger import.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.