orbitCardClass
plain-language theorem explainer
Orbit cardinality as a class function on combinatorial triangulation types: the number of labeled bounded complexes in a given relabeling class. Anyone deriving the discrete-gravity 1/|Aut| path-sum weight from pure gauge counting cites this. The definition is the quotient lift of the labeled orbit count, justified by the theorem that orbit size is invariant under gauge equivalence.
Claim. Let $c$ be a combinatorial triangulation class (the quotient of bounded labeled complexes by relabeling isomorphism). Define $\mathrm{orbitCard}(c)\in\mathbb{N}$ to be the number of labeled complexes gauge-equivalent to any representative of $c$. The value is independent of the representative because gauge-equivalent complexes have equal orbit sizes.
background
This module derives the standard 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 type of bounded complexes on the polarized interface edge set $B$. Two complexes are equivalent when a concrete relabeling witness exists between them.
gaugeOrbitCard K is the size of $K$'s relabeling orbit: the number of labeled complexes gauge-equivalent to $K$. Combinatorially distinct triangulations form the quotient TriangulationClass B by the relabeling setoid. The upstream congruence states that orbit count is a class function: if $K\sim K'$ then the two orbit cardinalities agree, via a subtype equivalence that rewrites membership using symmetry and transitivity of equivalence.
The companion counting quantity is pair count (labeled copy times concrete gauge witness). Their ratio on the quotient is the counting-defined class mass.
proof idea
One-line quotient lift: apply Quotient.liftOn to the class $c$, using the labeled orbit cardinality on representatives, and discharge well-definedness with the class-function theorem gaugeOrbitCard_congr. No further arithmetic; the body is exactly that lift.
why it matters
This is the numerator of the counting-defined class mass: labeled copies per unit of gauge volume, written only in terms of orbit and pair counts. Downstream, gaugeOrbitMass is their real ratio; existence (gaugeOrbitMass_mul_pairCount) and uniqueness (gaugeCountingMass_unique) pin any mass satisfying $\nu(c)\cdot\mathrm{pairCount}(c)=\mathrm{orbitCard}(c)$ to that ratio. Combined with orbit-stabilizer factorization of pair count, the mass equals $1/|\mathrm{Aut}|$.
The diagnostic identity labeledZ_eq_orbitWeighted_classSum rewrites the labeled path sum as a class sum weighted by orbit size times this counting mass, so the measure in $Z$ is carried entirely by counting data. The grounding theorem packages the whole preflight (torsor, factorization, derivation, uniqueness). In the Seven Gaps gravity stack this closes the gap between the postulated Aut-measure and a definition that never mentions Aut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.