pairCountClass_mk
plain-language theorem explainer
Evaluating the class-level gauge volume on the relabeling class of a labeled complex recovers the labeled pair count. Anyone working the orbit-stabilizer derivation of the 1/|Aut| measure cites this as the quotient-unfold step. Proof is definitional reflexivity from the lift.
Claim. For any bounded complex $K$ at bound $B$, the gauge-volume function on triangulation classes satisfies $\mathrm{pairCountClass}([K]) = \mathrm{pairCount}(K)$, where $[K]$ is the class of $K$ under the relabeling equivalence.
background
The module derives the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure gauge counting, rather than postulating it. Configurations are BoundedComplex B: combinatorial equilateral triangulations with at most $B$ vertices, edges, and tetrahedra.
Two counting quantities are defined without mentioning $\mu$ or automorphisms. The orbit card counts labeled complexes equivalent to $K$. The pair count is the gauge volume: number of pairs $(K', r)$ with $K'$ in the orbit and $r$ a concrete relabeling $K \to K'$. The relabeling relation is a setoid, so one quotients to triangulation classes.
pairCountClass is the lift of pair count to that quotient, well-defined by the congruence that equivalent complexes have equal pair counts. This lemma is the evaluation identity for that lift on a canonical representative.
proof idea
One-line definitional proof (rfl). By construction, pairCountClass is Quotient.liftOn of pairCount along the relabeling setoid, using pair-count congruence on equivalent pairs. The computation rule for liftOn on Quotient.mk therefore reduces the left-hand side to pairCount K by definition.
why it matters
Feeds the main derivation theorem gaugeOrbitMass_eq_mu: the counting-defined class mass equals the postulated measure $\mu K = 1/|\mathrm{Aut}, K|$. That proof unfolds the class mass, rewrites via the orbit-card and pair-count evaluation lemmas (this one among them), then applies the factorization pairCount = orbitCard · |Aut| from the torsor/orbit-stabilizer package.
In the Seven Gaps gravity track this closes the gap between a hand-written $1/|\mathrm{Aut}|$ weight and a mass defined only from orbit size over gauge volume. The model premise remains the pair-counting principle itself; once that is chosen, orbit-stabilizer forces the symmetry factor. No new Recognition landmark (T0–T8, RCL, $\varphi$) is invoked here: the result is pure finite-group counting on the triangulation setoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.