mu_congr
plain-language theorem explainer
Equivalent bounded complexes have equal symmetry-factor measure: a relabeling isomorphism forces μ(K)=μ(K'). Cited wherever the labeled path-sum Z_RS or the class-mass pushforward treats μ as a class function on triangulation fibers. Proof is a short term argument: the relabeling induces a bijection of automorphism groups, so the finite cardinals (and their reciprocals) agree.
Claim. Let $K,K'$ be bounded combinatorial complexes of size bound $B$. If there exists a relabeling isomorphism between them, then their symmetry-factor measures agree: $\mu(K)=\mu(K')$, where $\mu(K)=1/|\mathrm{Aut}(K)|$.
background
Lane 2 of the Seven Gaps gravity stack builds a proved path-sum measure on a scoped configuration class. Configurations are BoundedComplex B: incidence data (vertex/edge/tet counts capped by $B$, plus abstract incidence maps), modeled CDT-style with edge length fixed at the substrate mesh so geometry is purely combinatorial.
Two complexes are equivalent when a relabeling isomorphism exists (bijections of the three index sets that commute with incidence). The labeled measure is the standard discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut}(K)|$. Automorphism groups are finite and nonempty, so $0<\mu(K)\le 1$. The path sum is the finite sum $Z=\sum_K \mu(K),w(K)$ over the labeled class; for $Z$ and the pushforward class mass to be compatible with the relabeling quotient, $\mu$ must be constant on equivalence classes.
proof idea
Unpack the equivalence hypothesis to a witness relabeling isomorphism $r$. Unfold $\mu$ to the reciprocal of automorphism-group cardinality. The relabeling carries an automorphism-group congruence autCongr; rewrite with Nat.card_congr to equate the two finite cardinals, hence the two measures. No further arithmetic.
why it matters
This is the class-function property of the labeled measure in the proved $Z_{\mathrm{RS}}$ package. Downstream, classMass_eq_fiberCard_mul_mu factors pushforward class mass as fiber cardinality times $\mu$ of a representative, explicitly invoking this constancy; the T3 fork verdict ($\mu$ strictly below class mass on the $B=2$ edge class) and the Freudenthal-torus class-mass identities reuse it the same way. Cap-to-shell bridge theorems transport measure across exact-shell images via the same invariance.
Together with relabel-invariance of $Z$, it discharges the module's "measure respects the equivalence" bullet and makes the labeled sum compatible with the quotient view of triangulation classes. It does not close the still-open exponential-growth semantics for exact simplicial subclasses (finiteness of the superclass is what is proved).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.