Z_relabel_invariant
plain-language theorem explainer
The path sum Z over bounded complexes is unchanged when the weight is precomposed with any bijection that sends each complex to a relabeling-equivalent one. No invariance of the weight itself is required: only the 1/|Aut| measure needs to respect equivalence. Anyone building a class-function or quotient form of Z_RS cites this. The proof rewrites μ by mu_congr, then reindexes the finite sum along the bijection.
Claim. Fix a size bound $B\in\mathbb{N}$ and a weight $w$ on bounded complexes of size at most $B$. Let $\sigma$ be any bijection of that finite configuration set such that each $K$ is relabeling-equivalent to $\sigma(K)$. Then $Z_B(w\circ\sigma)=Z_B(w)$, where $Z_B(w)=\sum_K \mu(K)\,w(K)$ and $\mu(K)=1/|\mathrm{Aut}(K)|$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for the scoped recognition sum $Z_{\mathrm{RS}}$. Configurations are BoundedComplex B: combinatorial incidence data (vertex/edge/tet counts capped by $B$, edge and tet vertex maps) with the metric field dropped. The substrate fixes edge length at the minimum mesh, so the class is CDT-style and equilateral; it contains all bounded triangulations and also non-simplicial incidence data.
Two complexes are equivalent when a relabeling isomorphism exists between them. The automorphism group of a labeled complex is the set of self-relabelings; it is finite and nonempty, so the symmetry factor $\mu(K)=1/|\mathrm{Aut}(K)|$ is well-defined in $(0,1]$. The path sum is the finite sum $Z_B(w)=\sum_K \mu(K),w(K)$ over the Fintype of labeled complexes, with no convergence hypothesis.
Upstream, mu_congr already shows $\mu$ is constant on equivalence classes: equivalent complexes have equal measure, via cardinality transport along the induced automorphism-group isomorphism.
proof idea
Unfold the definition of $Z$. The left-hand sum is $\sum_K \mu(K),w(\sigma K)$. Pointwise, $\mu(K)=\mu(\sigma K)$ by mu_congr applied to the hypothesis that $K$ is equivalent to $\sigma(K)$; Finset.sum_congr lifts that equality into the sum. The resulting sum $\sum_K \mu(\sigma K),w(\sigma K)$ is exactly the original sum $\sum_K \mu(K),w(K)$ after reindexing by the bijection $\sigma$, via Fintype.sum_equiv (the summand identity is definitional). No property of $w$ is used.
why it matters
This is the invariance half of the honest scoped $Z_{\mathrm{RS}}$ package listed in the module status block: the $1/|\mathrm{Aut}|$ measure respects relabeling equivalence, so $Z$ is stable under any equivalence-preserving reindexing of the labeled class. Downstream, zRS_scoped_wellDefined packages unit-modulus unitary weights $\exp(i S)$, UV bounds $|Z|\le\mathrm{card}$, weight-level relabeling invariance under an action hypothesis, and this reindexing invariance into one theorem for the scoped class.
It also underwrites the class-function story: when $w$ itself is constant on equivalence classes, the summand $\mu\cdot w$ descends to the finite quotient TriangulationClass B. In the broader RS gravity lane this is the combinatorial skeleton of a CDT-style path integral at fixed lattice scale, with finiteness discharged rather than postulated. The sharper exponential-growth semantics of growthBase for exact simplicial subclasses remains open; this lemma does not touch that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.