stab2_card
plain-language theorem explainer
Permutations of a finite set of size m+2 that fix two prescribed distinct points number exactly m!. Gravity and combinatorics of labeled complexes cite it when counting automorphisms of a dust glued to a single edge. The proof reduces the stabilizer to the full symmetric group on the remaining m points via subtype equivalences and a cardinality computation.
Claim. For every natural number $m$ and every pair of distinct indices $p,q$ in a set of cardinality $m+2$, the number of permutations of that set that fix both $p$ and $q$ equals $m!$.
background
The ambient module derives the gluing law for Gap 2 rather than assuming it. Two premises drive the argument: size-blindness of the labeled weight (dependence only on the three index sizes) and multiplicativity of class mass over disjoint unions. Orbit counts then produce a binomial interleaving factor; cancelling them yields the three-variable shuffle identity whose solutions are inverse-factorial gauge weights.
A single edge is the two-vertex, one-edge complex used as a rigid building block. The present count is the stabilizer of its two endpoints inside the symmetric group on a larger labeled vertex set: once two distinct vertices are pinned, only the remaining $m$ labels may move freely. Upstream, the singleton-cardinality fact is the elementary Finset identity used when removing ${p,q}$ from the universe.
proof idea
Work classically. First rewrite the pointwise conditions $\sigma p=p$ and $\sigma q=q$ as the equivalent statement that $\sigma$ fixes every point outside the complement of ${p,q}$. The resulting subtype of permutations is equivalent, by Equiv.subtypeEquivRight, to the same fixed-point condition written with a universal quantifier.
A second equivalence, the inverse of Equiv.Perm.subtypeEquivSubtypePerm, identifies that subtype with the full symmetric group on the subtype ${y\mid y\neq p\land y\neq q}$. The Fintype cardinality of the latter subtype equals $m$: filter the universe, rewrite the filter as the set difference of the universe by the two-element set ${p,q}$, apply Finset.card_sdiff together with the singleton-card lemma and the hypothesis $p\neq q$, then finish by arithmetic. Transporting cardinality along the composite equivalence and invoking Fintype.card_perm yields $m!$.
why it matters
The result is the combinatorial engine behind the rigid dust-edge family. Downstream, autCard_dust_edge applies it (after an automorphism-equivalence that isolates the two edge endpoints) to conclude that the automorphism group of the disjoint union of an $a$-point dust with a single edge has cardinality $a!$. That identity is the availability statement for family (b) in the gluing derivation: automorphism counts multiply over dust-edge gluings, supplying the inverse-factorial factor required by the gauge-counting principle.
In the larger Gap-2 programme this closes one of the three rigid families needed so that gluing multiplicativity plus size-blindness force the shuffle solutions $f(a,b,c)=x^a y^b z^c/(a!b!c!)$, rather than leaving the gluing law as an axiom. It does not itself invoke Recognition landmarks (T5–T8, RCL, $\phi$), but it is pure finite-group input to the gravity-side counting that those landmarks later calibrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.