edgeCommOK
plain-language theorem explainer
Boolean check that a vertex permutation and an edge permutation jointly preserve a fixed ordered incidence map on two directed edges among four vertices. Hostile-probe Aut counters filter the full product of symmetric groups by this predicate. The body is a single decidable universal quantifier over the two edges.
Claim. Given an incidence map $ev:\{0,1\}\to\{0,1,2,3\}\times\{0,1,2,3\}$, a vertex permutation $\sigma_v$ of four labels, and an edge permutation $\sigma_e$ of two labels, return true iff for every edge $e$ one has $ev(\sigma_e(e))=(\sigma_v\times\sigma_v)(ev(e))$.
background
Gap2 work in the SevenGaps gravity stack studies label-erasure and fibre counts for small directed complexes. The carrier here is deliberately tiny: two edges and four vertices, with incidence recorded as an ordered pair map $ev:\mathrm{Fin},2\to\mathrm{Fin},4\times\mathrm{Fin},4$.
The ordered edge-commutation predicate asks whether a candidate pair $(\sigma_v,\sigma_e)$ pushes incidence forward consistently: permuting the edge index and then reading $ev$ must equal applying $\sigma_v$ to both endpoints of the original incidence. No automorphism type is introduced; the check is a plain Boolean on permutation pairs.
This module is an uncommitted adversarial probe of Gap2LabelErasure (attacks on G1 dependency, definitional collapse, directed Aut recomputation by kernel enumeration, and vacuity). The same predicate appears upstream in Gap2PoissonCoarea as the ordered edge-commutation test used to enumerate Aut candidates without building an Aut structure.
proof idea
Definitional, not a proof. The body hands the universal statement $\forall e:\mathrm{Fin},2,; ev(\sigma_e e)=\mathrm{Prod.map},\sigma_v,\sigma_v,(ev e)$ to decide, which discharges it by finite enumeration over the two edge indices. Prod.map applies the vertex permutation to both coordinates of the ordered endpoint pair. No lemmas are invoked.
why it matters
Local Aut counters twoEdgeAutCount and pathPlusAutCount filter the full product $\mathrm{Sym}_4\times\mathrm{Sym}_2$ by this Boolean, yielding the directed kernel sizes used in the hostile probe. Downstream native_decide theorems pin the two-edge case: identity and component swap succeed, while pure edge reversal fails, so the directed carrier admits exactly two ordered Aut candidates rather than an undirected flip.
That distinction feeds the class-mass / $\mu$ ratio argument in the probe (enumerated ratio $1/2$, not the undirected $1/4$). The predicate is the computational stand-in for "ordered incidence automorphism" while Gap2 label-erasure and Poisson-coarea fibre counts are under adversarial recomputation. It does not itself close a forcing-chain landmark; it is scaffolding for the directed-Aut attack surface of Gap2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.