Z_norm_le_muSum
plain-language theorem explainer
The modulus of the recognition path sum is at most the total symmetry-factor measure whenever every configuration weight has complex modulus at most one. Path-integral and gravity workers cite it for UV control of the scoped Z_RS sum over bounded complexes. The argument is a finite triangle inequality plus the elementary bound |μ w| ≤ μ from positivity of μ and |w| ≤ 1.
Claim. Fix $B \in \mathbb{N}$ and a weight $w$ on the finite class of bounded combinatorial complexes of size at most $B$. If $\|w(K)\| \le 1$ for every such $K$, then $\|Z(B,w)\| \le \sum_K \mu(K)$, where $Z(B,w) = \sum_K \mu(K)\, w(K)$ and $\mu(K) = 1/|\mathrm{Aut}(K)|$.
background
Lane 2 of the Seven Gaps gravity stack builds a proved path-sum measure for the recognition partition function $Z_{\mathrm{RS}}$ on a scoped class of configurations. 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; the substrate fixes edge length at the minimum mesh). The class is finite as a Fintype.
The symmetry-factor measure is $\mu(K) = 1/|\mathrm{Aut}(K)|$. Automorphism groups are finite and nonempty, so $0 < \mu(K) \le 1$, and $\mu$ is invariant under relabeling. The path sum is the finite complex sum $Z(B,w) = \sum_K \mu(K), w(K)$; finiteness needs no convergence hypothesis.
This lemma is the $\mu$-weighted modulus bound stated in the module: for weights of modulus at most one, $|Z|$ is controlled by the total measure $\sum \mu$.
proof idea
Unfold the definition of $Z$. Apply the finite-sum triangle inequality (norm_sum_le) to get
$|\sum_K (\mu K), w(K)| \le \sum_K |(\mu K), w(K)|$.
Termwise, rewrite $|(\mu K), w(K)| = \mu(K),|w(K)|$ via multiplicativity of the complex norm, reality of $\mu$, and positivity $\mu(K) > 0$ (so the absolute value drops). The hypothesis $|w(K)| \le 1$ then yields $\mu(K),|w(K)| \le \mu(K)$ by multiplying a positive quantity by a factor at most one. Summing finishes the bound.
why it matters
This is one of the core proved modulus controls for the honest scoped $Z_{\mathrm{RS}}$ in Seven Gaps Lane 2. Together with the coarser card bound $|Z| \le |\mathrm{BoundedComplex}, B|$ and the unitary instance $w(K) = e^{i S(K)}$, it discharges UV-finiteness of the path sum on the bounded class: a finite sum with an explicit proved bound, replacing the postulated growthBase^N count in the older PathSumUVBound.AdmissibleTriangulationFamily interface.
The module tags this as a zero-sorry theorem in the proved tier (alongside finiteness of the labeled class, the relabeling setoid, and relabeling invariance of $Z$). It does not close the sharper exponential-growth semantics for exact simplicial subclasses; that remains open. No downstream Lean dependents are recorded yet; the natural consumers are the card bound, the unitary well-definedness statement, and any later continuum or continuum-limit comparison that needs a uniform modulus estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.