pairCount_congr
plain-language theorem explainer
Gauge-equivalent bounded complexes have identical pair counts: the (orbit copy, relabeling witness) volume is a class function. Anyone lifting gauge volume to triangulation classes, or proving the counting mass equals 1/|Aut|, cites this. The proof factors pair count as orbit size times automorphism order, then applies the two congruence lemmas for those factors.
Claim. Let $K$ and $K'$ be bounded complexes on the same bound $B$. If $K$ and $K'$ are gauge-equivalent (there exists a relabeling witness between them), then their pair counts agree: the number of pairs $(K'', r)$ with $K''$ in the relabeling orbit and $r$ a concrete gauge witness equals the same number computed from $K'$.
background
This module derives the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure gauge counting, rather than postulating it. Two raw counts are defined without mentioning $\mu$ or $\mathrm{Aut}$: the orbit cardinality (number of labeled complexes equivalent to $K$ inside the bounded universe) and the pair count (number of pairs consisting of an orbit member together with a concrete relabeling witness). The pair count is the gauge volume of the orbit.
Orbit-stabilizer is already proved in-module: relabeling witnesses form a torsor over the automorphism group, so pair count factors as orbit cardinality times $|\mathrm{Aut}, K|$. Separate congruence lemmas show that both orbit cardinality and automorphism order are unchanged under equivalence. The present result packages those into class-function status for the pair count itself.
The ambient setting is the Seven Gaps gauge-preflight layer: quantities must descend to the quotient of bounded complexes by gauge equivalence before a class-level mass can be defined.
proof idea
Term-style rewrite proof. Expand both sides with the factorization lemma that writes pair count as orbit cardinality times automorphism order. Replace the two orbit-cardinality factors by the orbit-cardinality congruence under the given equivalence, and the two automorphism-order factors by the automorphism-order congruence. Equality of the products follows immediately; no further arithmetic is needed.
why it matters
Representative independence of pair count is one of the three class-function lemmas the module lists as proved (alongside orbit-cardinality and representative-mass congruence). Downstream, the quotient lift that defines gauge volume on triangulation classes uses this theorem as the well-definedness proof for Quotient.liftOn. The representative-level mass ratio (orbit card over pair count) rewrites both numerator and denominator through this result and the orbit congruence, yielding a class function that later equals $1/|\mathrm{Aut}|$ under the pair-counting principle.
In the Recognition gravity stack this closes the preflight step that turns labeled counting into a gauge-invariant measure on complexes, the discrete analogue of dividing by gauge volume before summing over geometries. It does not itself force spacetime dimension or the eight-tick structure; those sit upstream in the forcing chain. It does make the derived $1/|\mathrm{Aut}|$ mass honest on the quotient rather than representative-dependent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.