relabelingCount
plain-language theorem explainer
Counts the finite set of concrete relabeling witnesses between two bounded complexes K and K'. Gravity and discrete-path-sum authors cite it when converting orbit-stabilizer into a pure counting identity. The body is a one-line cardinality wrapper: Nat.card of the Relabel type.
Claim. For bounded complexes $K,K'$ in the fixed bound $B$, the relabeling count is the natural number $|\mathrm{Relabel}(K,K')|$, i.e. the number of concrete gauge witnesses taking $K$ to $K'$.
background
This module sits in the Seven Gaps gauge-preflight layer. PathSumMeasure postulates the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$. ExactShellGaugePreflight instead derives that factor from pure counting quantities that never mention $\mu$ or $\mathrm{Aut}$ in their definitions.
A bounded complex is a labeled triangulation living inside a finite universe of size $B$. Two complexes are equivalent when a relabeling witness exists; $\mathrm{Relabel}(K,K')$ is the type of such witnesses. The automorphism group $\mathrm{Aut},K$ is the special case $K'=K$.
Sibling counters build on this: gauge-orbit cardinality counts labeled copies equivalent to $K$, and pair count totals pairs (copy, witness). Orbit-stabilizer then factorizes pair count as orbit size times $|\mathrm{Aut},K|$.
proof idea
Pure definitional wrapper. Unfolds to $\mathrm{Nat.card}(\mathrm{Relabel},K,K')$. No lemmas, no tactics; noncomputable only because finite cardinalities of types are noncomputable in general.
why it matters
This is the witness-side counter in the gauge-volume story. The theorem relabelingCount_eq_autCard (orbit-stabilizer, cardinal form) states that for equivalent $K,K'$ the count equals $|\mathrm{Aut},K|$, via the torsor equivalence torsorEquiv. That identity feeds pairCount_eq_orbitCard_mul_autCard and ultimately gaugeOrbitMass_eq_mu, which derives $\mu=1/|\mathrm{Aut}|$ from counting alone.
The grounding theorem gaugePreflight_grounded packages the same equality as the first conjunct of its status flags. In the broader RS gravity stack this closes the gap between postulated path-sum measure and a definition that only names Equivalence and Relabel, keeping the $1/|\mathrm{Aut}|$ factor as a theorem rather than an axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.