twoEdge_autCount_eq_two
plain-language theorem explainer
Two disjoint directed edges admit exactly two ordered automorphism candidates under the directed edge-commuting filter. Gravity and coarea arguments cite this kernel count when converting Aut orders into fibre and class-mass ratios. The equality is discharged by exhaustive native decision on the finite filtered Finset of vertex/edge permutations.
Claim. The number of ordered directed automorphism candidates of the two-edge witness complex equals $2$. Equivalently, filtering the product of permutations of four vertices and two edges by the edge-commutation predicate for that witness yields a set of cardinality $2$.
background
This module is an uncommitted adversarial probe of Gap2 label-erasure: it recomputes directed Aut counts by kernel enumeration and checks whether G1/G2 fibre and measure flags move under hostile redefinitions.
The two-edge witness is a bounded labeled complex with four vertices and two directed edges (two disjoint arcs). An ordered Aut candidate is a pair of permutations (vertex relabeling in $S_4$, edge relabeling in $S_2$) that preserves ordered incidence under the edge-commutation predicate. The count twoEdgeAutCount is the cardinality of that filtered Finset.
Upstream, Aut of a labeled complex is the set of self-relabelings. Parallel definitions in the Poisson-coarea module use the same kernel enumeration so that inverse-Aut ratios can be compared to fibre ratios via orbit-stabilizer arithmetic.
proof idea
One-line decision proof: native_decide evaluates the finite Finset filter defining the Aut-candidate count and checks that its cardinality is definitionally $2$. No algebraic lemmas are invoked; the witness is small enough that exhaustive enumeration closes the equality.
why it matters
The count feeds every place that needs the directed Aut order of the two-edge witness. Downstream, the enumerated class-mass/mu ratio becomes $1/2$ (not the undirected $1/4$), the inverse-Aut ratio equals $1/2$, and the scoped coarea identity at the two-edge witness equates order-erasure weight times fibre cardinality to the reciprocal Aut order.
In the Seven Gaps gravity stack this is the directed half of the Aut bookkeeping behind label erasure and Poisson coarea. It supports the claim that directed Aut recomputation does not move the measure flag, while leaving broader coarea claims (e.g. full C23) explicitly unclaimed. It is local combinatorics, not a forcing-chain step (T0–T8), but it stabilizes the Aut denominators used when gap-side measures are compared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.