Z_norm_le_card
plain-language theorem explainer
For any complex weight of modulus at most one on the bounded combinatorial complexes of size cap B, the recognition path sum Z has modulus at most the finite cardinality of that configuration class. Gravity and path-integral workers cite it as the explicit UV-finiteness bound that replaces an assumed exponential growth count. The proof is a short triangle-inequality calc: each mu-weighted term is at most 1, so the sum is at most the number of labeled complexes.
Claim. Fix a size bound $B\in\mathbb{N}$ and a weight $w$ on bounded combinatorial complexes of size at most $B$ with $\|w(K)\|\le 1$ for every configuration $K$. Then the path sum $Z_B(w)=\sum_K \mu(K)\,w(K)$, with symmetry factors $\mu(K)=1/|\mathrm{Aut}(K)|$, satisfies $\|Z_B(w)\|\le \#\{\text{bounded complexes of size}\le B\}$.
background
Lane 2 of the Seven Gaps gravity program builds a proved path-sum measure for the recognition partition function $Z_{\mathrm{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; the substrate fixes edge length at the minimum mesh). The class is a Fintype, so every sum over it is finite by construction.
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)$. Module status tags this as a proved UV-finiteness bound that discharges the count-finiteness content formerly assumed via a growthBase field on admissible triangulation families; sharper exponential-growth semantics for exact simplicial subclasses remain open.
proof idea
Unfold the definition of $Z$. Apply the triangle inequality norm_sum_le to pass the modulus inside the sum. For each summand, factor $|\mu(K)\cdot w(K)|=\mu(K),|w(K)|$ (using positivity of $\mu$ so the real norm is $\mu$ itself). Bound by $1\cdot 1$ via mu_le_one and the hypothesis $|w(K)|\le 1$, then simplify. The resulting constant sum of ones equals the universe cardinality of BoundedComplex B by Finset.sum_const and nsmul_eq_mul. No special structure of $w$ beyond the modulus bound is used.
why it matters
This is one of the two modulus bounds that make the scoped path sum honest: $|Z|\le\sum\mu$ and the coarser $|Z|\le\mathrm{card}$. Downstream, zRS_scoped_wellDefined packages the unitary instance $w(K)=\exp(i S(K))$ for a real action $S$: unit-modulus weights, relabeling invariance of the weight, the card bound on $|Z_{\mathrm{RS}}|$, and invariance under equivalence-preserving reindexing. That theorem is the honest $Z_{\mathrm{RS}}$ statement for the scoped class.
In the Recognition framework this closes the UV-count gap for gravity path sums on bounded complexes: finiteness is proved rather than postulated. It does not yet force the sharper simplicial growth law; the module explicitly leaves exponential-growth semantics for exact triangulations open. Parent context is Seven Gaps Lane 2, feeding any later continuum or continuum-limit claims that need a finite discrete measure first.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.