gaugeOrbitCard_congr
plain-language theorem explainer
If two bounded complexes are gauge-equivalent, they have the same number of labeled copies in their relabeling orbit. Anyone lifting orbit counts to triangulation classes cites this. The proof is a one-shot cardinality transport along the subtype equivalence induced by symmetry and transitivity of Equivalent.
Claim. Let $K$ and $K'$ be bounded complexes of bound $B$. If $K$ and $K'$ are gauge-equivalent (there exists a relabeling witness between them), then the number of labeled complexes equivalent to $K$ equals the number equivalent to $K'$: $|\mathrm{orbit}(K)| = |\mathrm{orbit}(K')|$.
background
This module derives the discrete-gravity symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$ from pure gauge counting, rather than postulating it. The orbit count gaugeOrbitCard K is the number of labeled complexes inside the bounded universe that are equivalent to $K$ (the size of $K$'s relabeling orbit). The companion count pairCount K tallies pairs $(K', r)$ with $K'$ in that orbit and $r$ a concrete relabeling witness; their ratio is the gauge mass.
Equivalence of complexes is the relation "there exists a relabeling" on BoundedComplex B. The module already has reflexivity, symmetry, and transitivity for that relation. Class-function lemmas such as this one are the preflight needed before any quantity can descend to the quotient TriangulationClass B.
Upstream, the torsor/orbit-stabilizer package shows that for equivalent complexes the witness set is a torsor over the automorphism group, so pair counts factor as orbit size times $|\mathrm{Aut}|$. Representative independence of the orbit size is the first half of making the mass well-defined on classes.
proof idea
Term-mode proof via Nat.card_congr. Build a subtype equivalence on the right: a labeled complex $L$ lies in the orbit of $K$ if and only if it lies in the orbit of $K'$, because Equivalent is symmetric and transitive.
Concretely, Equiv.subtypeEquivRight packages the two directions
$L \sim K \Rightarrow L \sim K'$ (compose with the given witness after symmetry) and
$L \sim K' \Rightarrow L \sim K$ (compose with the given witness). Cardinality is invariant under that bijection, so the two orbit cards agree.
why it matters
Representative independence of the orbit count is required before the quotient lifts exist. Downstream, orbitCardClass is exactly Quotient.liftOn of the orbit card using this congruence; pairCount_congr rewrites through it together with automorphism-card congruence; and gaugeMassRep_congr divides the two class functions to get a representative-independent mass ratio.
That mass ratio is what the module equates to $\mu = 1/|\mathrm{Aut}|$ under the pair-counting principle (gaugeOrbitMass_eq_mu). In the Seven Gaps gravity stack this is the gauge-preflight step that turns a postulated symmetry factor into a derived counting identity. Gap2 gluing reuses the same invariance for uniform weights on classes.
No forcing-chain landmark (T5–T8) is at stake here; the result is pure discrete-gauge bookkeeping inside the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.