zRS_scoped_wellDefined
plain-language theorem explainer
For any real action S that is constant on relabeling-equivalent bounded complexes, the unitary path-sum weights exp(i S) have modulus one, inherit the same invariance, and the finite measure Z_RS obeys ‖Z‖ ≤ card(BoundedComplex B) and is unchanged under any equivalence-preserving reindexing. Gravity and path-sum UV arguments cite this as the honest well-definedness package for Z_RS on the scoped class. The proof packages four prior lemmas via a four-way refine.
Claim. Fix a bound $B\in\mathbb{N}$ and a real action $S$ on the finite class of bounded complexes of size at most $B$. Assume $S$ is constant on relabeling-equivalent complexes. Then: (i) every unitary weight $w_K=\exp(i\,S(K))$ has $|w_K|=1$; (ii) $w$ is constant on equivalence classes; (iii) the path sum $Z_B(w)=\sum_K \mu(K)\,w_K$ satisfies $\|Z_B(w)\|\le |\mathrm{BoundedComplex}_B|$; (iv) if $\sigma$ is any bijection of the class that preserves equivalence, then $Z_B(w\circ\sigma)=Z_B(w)$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for $Z_{RS}$ on a scoped configuration class. A BoundedComplex B is a combinatorial triangulation at fixed lattice scale: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps and no metric field (CDT-style; edge length fixed at the substrate mesh). The class is finite by an explicit coding equivalence, so every sum over it is a finite sum with no convergence hypothesis.
Two complexes are equivalent when a relabeling isomorphism exists; that relation is a proved setoid. Automorphism groups are finite and nonempty, so the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ satisfies $0<\mu(K)\le 1$ and is relabeling-invariant. The path sum is $Z_B(w)=\sum_K \mu(K),w(K)$. Prior results already give the modulus bounds $|Z|\le\sum\mu$ and $|Z|\le\mathrm{card}$, plus invariance of $Z$ under any equivalence-preserving bijection of configurations.
The unitary instance takes $w(K)=\exp(i,S(K))$ for a real action $S$. This theorem packages the four well-definedness properties of that instance once $S$ itself is assumed relabeling-invariant.
proof idea
Term-mode four-way refine. The first conjunct is the existing lemma that unitary weights have modulus one. The second unfolds the unitary weight and rewrites by the hypothesis that $S$ is constant on equivalent complexes. The third applies the general UV bound $|Z|\le\mathrm{card}$ to the unitary weights, feeding the unit-modulus fact as the pointwise bound. The fourth is a direct application of the already-proved relabeling invariance of $Z$ under equivalence-preserving bijections.
why it matters
This is the honest $Z_{RS}$ statement for the scoped class: unit weights, weight-level invariance, the proved UV-finiteness bound $|Z|\le\mathrm{card}$, and measure-level reindexing invariance, all with zero sorry and no new axioms. It discharges the well-definedness content needed before growth-base and shell-gauge arguments can treat $Z_{RS}$ as a finite complex measure rather than a formal series.
Downstream, ExactShellGaugeUV uses the surrounding measure package (including class-level $\mu\le 1$) when descending labeled data to quotient classes; the doc there notes that a GlobalEquivalent-invariant labeled action descends to a class function in the same style as the $hS$ hypothesis here. In the broader Seven Gaps gravity lane, the result replaces an assumed exponential growthBase field of the admissible-family interface by a proved finite cardinal of the scoped superclass; sharper exponential-growth semantics for exact simplicial subclasses remain open. Framework contact is the path-sum side of recognition gravity, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.