orbitCardClass_mk
plain-language theorem explainer
On the quotient of bounded complexes by relabeling, the class-level orbit cardinality of the class of K equals the labeled gauge-orbit size of K. Anyone unfolding class mass or simplifying gauge counting cites this. The equality is definitional: a one-line reflexivity proof from the quotient lift.
Claim. For every bounded complex $K$ in the finite universe of bound $B$, the orbit-cardinality function on the relabeling quotient satisfies $\mathrm{orbitCard}([K]) = |\{K' : K' \sim K\}|$, i.e. it recovers the number of labeled complexes gauge-equivalent to $K$.
background
This module derives the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure gauge counting, rather than postulating it as in PathSumMeasure. The raw counting ingredient is the labeled orbit size: how many complexes in the finite universe BoundedComplex B are gauge-equivalent to a fixed $K$ under vertex relabeling.
That quantity is gaugeOrbitCard K, defined as the cardinality of ${K' // \mathrm{Equivalent}, K, K'}$. Classes live on the quotient by the relabeling setoid; orbitCardClass is the corresponding class function on triangulation classes. The module's status note lists representative independence among the proved ingredients needed before the mass derivation can run.
Upstream, gaugeOrbitCard is already known to be positive and finite because the ambient universe is a Fintype. The present lemma is the bridge that evaluates the lifted class function on a concrete representative.
proof idea
Term proof by rfl. By construction, orbitCardClass is the quotient lift of gaugeOrbitCard along the relabeling setoid, so applying it to Quotient.mk of $K$ is definitionally gaugeOrbitCard K. No lemmas are invoked; the simp attribute makes the reduction automatic in later rewrites.
why it matters
Parent use is gaugeOrbitMass_eq_mu, the module's main derivation: the counting-defined class mass equals the postulated $\mu K = 1/|\mathrm{Aut}, K|$. That proof unfolds gaugeOrbitMass, then rewrites with this lemma (and the twin for pair count) before applying orbit-stabilizer factorization pairCount = orbitCard · |Aut|.
Without the class-on-representative reduction, the mass on the quotient cannot be compared to the labeled Aut formula. In the Seven Gaps gravity stack this closes the preflight step that turns gauge volume counting into the $1/|\mathrm{Aut}|$ path-sum weight, the standard discrete-gravity convention now obtained rather than assumed. It is bookkeeping, but it is the bookkeeping the derivation rewrites through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.