summand_class_constant
plain-language theorem explainer
If a complex weight is invariant under relabeling, the measure-weighted summand μ·w is constant on each equivalence class of bounded complexes. Anyone assembling the recognition path sum Z over the finite quotient of triangulations cites this. The proof is a two-rewrite: μ is already a relabeling invariant, and the weight hypothesis supplies the rest.
Claim. Fix a bound $B\in\mathbb{N}$ and a weight $w$ on bounded complexes of size at most $B$. Suppose $w$ is constant on relabeling-isomorphic pairs. Then for any two equivalent complexes $K\sim K'$, one has $\mu(K)\,w(K)=\mu(K')\,w(K')$ in $\mathbb{C}$, where $\mu=1/|\mathrm{Aut}|$ is the symmetry-factor measure.
background
Lane 2 of the Seven Gaps program builds an honest, finite path-sum measure for the recognition partition function $Z_{\mathrm{RS}}$. Configurations live in the scoped class BoundedComplex B: combinatorial incidence data (vertices, edges, tetrahedra) capped by $B$, with edge length fixed at the substrate mesh, CDT-style. Relabeling isomorphism is a proved equivalence relation; its quotient is the finite set of combinatorially distinct triangulations.
The measure on labeled complexes is the classical symmetry factor $\mu(K)=1/|\mathrm{Aut} K|$, already shown positive, at most one, and invariant under relabeling ($\mu$-congruence). The path sum is the finite sum $Z(B,w)=\sum_K \mu(K),w(K)$ over the labeled Fintype; no convergence hypothesis is needed.
This lemma is the elementary bridge from labeled summands to class-constant summands: once both $\mu$ and $w$ are class functions, the product is too, so $Z$ factors through the quotient.
proof idea
One-line rewrite proof. Apply $\mu$-congruence along the given relabeling equivalence $K\sim K'$ to replace $\mu(K)$ by $\mu(K')$, then apply the invariance hypothesis on $w$ along the same equivalence to replace $w(K)$ by $w(K')$. The two sides match in $\mathbb{C}$.
why it matters
Without class-constancy of the summand, the labeled path sum cannot be rewritten as a sum over triangulation classes. The immediate parent is the diagnostic identity that equates the labeled $Z$ to an orbit-weighted class sum: $Z=\sum_c |\mathrm{orbit},c|\cdot m_{\mathrm{gauge}}(c)\cdot w(\mathrm{rep},c)$, with the measure carried entirely by counting data. That identity is the preflight step toward an exact shell-gauge form of $Z_{\mathrm{RS}}$.
In the broader Recognition framework this sits inside the gravity path-sum lane: a proved finite measure on bounded complexes, with the unitary instance $w=\exp(iS)$ (sinh recognition action on deficit data) supplying the honest scoped $Z_{\mathrm{RS}}$. Finiteness of the superclass already discharges the count-finiteness content of the older admissible-family growth postulate; sharper exponential growth for exact simplicial classes remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.