pairCountClass
plain-language theorem explainer
Gauge volume of a combinatorial triangulation class: the total number of (labeled copy, relabeling witness) pairs for any representative. Discrete-gravity workers cite it when the counting measure must live on classes rather than labeled complexes. Defined by lifting the representative-level pair count via the congruence that equivalent complexes share the same count.
Claim. For each combinatorial triangulation class $c$ (the quotient of bounded labeled complexes by relabeling isomorphism), the gauge volume of $c$ is the natural number equal to the pair count of any labeled representative of $c$. The value is independent of the choice of representative.
background
This module derives the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure gauge counting, without putting $\mu$ or $\mathrm{Aut}$ into the mass definition. The ambient universe is the finite set of bounded labeled complexes on the bichromatic interface edge set $B$ (the polarized diamond field's ordered edges).
A triangulation class is the quotient of those labeled complexes by the relabeling setoid: combinatorially distinct triangulations. At the labeled level, the pair count of $K$ is the cardinality of pairs $(K', r)$ with $K'$ equivalent to $K$ and $r$ a concrete relabeling $K \to K'$. That quantity is the gauge volume of the orbit; its definition mentions only equivalence and relabeling witnesses.
Upstream, pair-count congruence shows the gauge volume is a class function: equivalent complexes have equal pair counts (via orbit-stabilizer factorization into orbit card times automorphism order). That congruence is exactly what lets the count descend to the quotient.
proof idea
One-line quotient lift. Apply Quotient.liftOn to the class $c$, using the representative-level pair count as the function and pair-count congruence as the well-definedness proof: whenever two labeled complexes are equivalent, their pair counts agree, so the lift is independent of the chosen representative.
why it matters
This is the class-level gauge volume that the counting mass is built from. The gauge-orbit mass is defined as orbit-card class over this pair-count class (labeled copies per unit gauge volume), with no mention of $\mu$ or $\mathrm{Aut}$. Existence (gaugeOrbitMass_mul_pairCount) and uniqueness (gaugeCountingMass_unique) of the normalized counting measure both quantify over this quantity; positivity of the class pair count supplies the nonzero denominator.
Together with the orbit-stabilizer factorization pairCount = orbitCard * |Aut|, the derivation theorem identifies the counting mass with $1/|\mathrm{Aut}|$. The grounding theorem packages that chain. Downstream, the measure-substrate blocker also consumes the class pair count when stating the gauge-counting principle. In the Seven Gaps program this closes the preflight step that turns a postulated symmetry factor into a derived class measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.