edgeCommOK
plain-language theorem explainer
Boolean check that a vertex permutation and an edge permutation jointly preserve a fixed two-edge incidence map on four labeled vertices. Downstream Aut-count filters for the equal-census witnesses twoEdge and pathPlusIsolated use it as the ordered-commutation gate. The body is a single decide on the pointwise incidence identity.
Claim. Fix an incidence map $ev:\{0,1\}\to\{0,1,2,3\}^2$. For permutations $\sigma_v$ of the four vertices and $\sigma_e$ of the two edges, the predicate returns true if and only if $\forall e\in\{0,1\}$, $ev(\sigma_e(e))=(\sigma_v\times\sigma_v)(ev(e))$.
background
Gap 2 (lane C16) studies a LIFO max-name post/unpost process on tet-free bounded complexes. Every legal move has rate 1; rate symmetry plus irreducibility yield a uniform stationary law on each finite cap. At equal census $(4,2,0)$ the two Aut-distinct witnesses are the disjoint two-edge complex and the path-plus-isolated complex.
The C35 firewall forbids process-level mention of Aut, orbit, stabilizer, or gauge class. Those words appear only in conclusions. Accordingly this predicate never builds an automorphism type: it is a Boolean on a pair of ordinary permutations of the fixed label sets Fin 4 and Fin 2.
The incidence map $ev$ records, for each of the two named edges, its ordered endpoint pair. Commutation means the edge permutation conjugates incidence through the vertex permutation (componentwise on endpoints).
proof idea
Definition, not a theorem. The body is one decide applied to the decidable proposition $\forall e:\mathrm{Fin},2,, ev(\sigma_e e)=\mathrm{Prod.map},\sigma_v,\sigma_v,(ev e)$. No lemmas are invoked; Lean reduces the finite universal quantifier by computation.
why it matters
Supplies the filter predicate for the directed Aut-candidate enumerations twoEdgeAutCount and pathPlusAutCount (both here and in the hostile-probe twin module). Those cardinalities are the fibre sizes 2 and (implicitly) the matching count that produce the stationary class-mass ratio $1/2$ under uniform $\pi$ at census $(4,2,0)$.
Concrete native_decide theorems (twoEdge_id_ok, twoEdge_component_swap_ok, twoEdge_edge_flip_fails_comm) pin that exactly the identity and the component swap pass, while edge reversal fails, confirming the directed carrier (undirected flip absent). This is the ordered Aut correction that replaces an undirected $1/4$ guess by the measured $1/2$. Flag 8 and FullTheoryLedger stay untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.