pairCount_eq_orbitCard_mul_autCard
plain-language theorem explainer
For any bounded complex K, the gauge volume (count of pairs of an equivalent labeled copy and a concrete relabeling witness) equals the size of K's relabeling orbit times the order of Aut(K). Discrete-gravity and Seven-Gaps authors cite this as the orbit-stabilizer factorization that turns pure pair counting into the 1/|Aut| measure. The proof builds a sigma-to-product equivalence from the torsor structure of Relabel fibers and compares cardinalities.
Claim. For every bounded complex $K$ in the bounded universe of size $B$, the number of pairs $(K', r)$ with $K'$ gauge-equivalent to $K$ and $r$ a concrete relabeling $K\to K'$ equals the number of labeled complexes equivalent to $K$ times the number of automorphisms of $K$: $\mathrm{pairCount}(K)=\mathrm{gaugeOrbitCard}(K)\cdot|\mathrm{Aut}(K)|$.
background
This module sits in the Seven Gaps gauge-preflight layer. PathSumMeasure postulates the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut}(K)|$. Here that factor is derived from pure counting, without writing $\mathrm{Aut}$ into the mass definition.
Three counting quantities are primary. The orbit size gaugeOrbitCard K is the number of labeled complexes equivalent to $K$ inside the bounded universe. The gauge volume pairCount K counts pairs $(K',r)$ with $K'$ in that orbit and $r:\mathrm{Relabel},K,K'$ a concrete gauge witness; its definition mentions only equivalence and relabeling. Automorphisms $\mathrm{Aut},K$ are the self-relabelings of $K$.
Upstream, torsorEquiv shows that for equivalent $K,K'$ the set of relabeling witnesses is a torsor over $\mathrm{Aut},K$, so each fiber has cardinality $|\mathrm{Aut},K|$. The companion relabelingCount_eq_autCard records that fiber cardinality equality. The present theorem packages those facts into a global factorization of the pair count.
proof idea
Construct an equivalence between the sigma type of pairs (equivalent copy $K'$, relabeling $K\to K'$) and the product of the subtype of equivalent copies with $\mathrm{Aut},K$. On each fiber, apply the inverse of torsorEquiv (using classical choice on the equivalence witness) so the fiber is identified with $\mathrm{Aut},K$. Unfold pairCount and gaugeOrbitCard, then transport cardinality across the equivalence and split the product card via Nat.card_prod.
why it matters
This is the orbit-stabilizer step named in the module doc as the bridge from pair counting to $1/|\mathrm{Aut}|$. Downstream, gaugeOrbitMass_eq_mu rewrites the counting-defined class mass through this identity to recover $\mu(K)=1/|\mathrm{Aut},K|$. pairCount_pos and pairCount_congr inherit positivity and class-function status from the factorization. The grounding theorem gaugePreflight_grounded lists the factorization among the status-backed facts.
Outside the module, Gap2's orbitCard_mul_autCard rewrites the product as a factorial count of labelings, and orbitCard_dunion_of_autMul uses the same stabilizer arithmetic for binomial interleaving under disjoint union. In the Recognition gravity stack this closes the gauge-volume half of the Seven Gaps preflight: the measure is no longer an external discrete-gravity convention but a consequence of counting $(copy,witness)$ pairs plus torsor structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.