Z
plain-language theorem explainer
Defines the recognition path sum over the finite class of bounded labeled complexes of size at most B: a μ-weighted sum of a complex weight w. Anyone citing the scoped Z_RS measure, its modulus bounds, or relabeling invariance starts here. The body is a plain finite sum, so the object is well-defined with no convergence hypothesis.
Claim. For $B \in \mathbb{N}$ and a weight $w$ on the class of bounded labeled complexes of size at most $B$, set $Z(B,w) := \sum_K \mu(K)\, w(K)$, where the sum runs over all such complexes $K$ and $\mu(K)$ is the symmetry-factor measure $1/|\mathrm{Aut}(K)|$.
background
This module builds a proved path-sum measure for the scoped recognition partition function $Z_{\mathrm{RS}}$. Configurations are modeled by BoundedComplex B: combinatorial triangulations with at most $B$ vertices, edges, and tetrahedra, carrying only incidence data. The substrate fixes edge length at the minimum mesh, so geometries are equilateral (CDT-style); the metric field of the ambient Regge triangulation type is dropped and replaced by an explicit size cap.
The class is a Fintype via an explicit coding equivalence, so every sum over it is finite. The weight $\mu(K)=1/|\mathrm{Aut}(K)|$ is the standard symmetry factor: the automorphism group is finite and nonempty, giving $0<\mu(K)\le 1$, and $\mu$ is invariant under relabeling. The path sum is then the $\mu$-weighted sum of an arbitrary complex weight $w$ on that finite class.
Upstream, this discharges the count-finiteness content that PathSumUVBound.AdmissibleTriangulationFamily had only postulated via a growthBase field: a proved finite cardinal replaces a bound assumption for the superclass of bounded incidence data.
proof idea
Pure definition. The body is the finite sum $\sum_K (\mu(K):\mathbb{C})\cdot w(K)$ ranging over the Fintype instance on the bounded class. No lemmas are applied; well-definedness is immediate from finiteness of the index type. Downstream norm and invariance theorems treat this sum as the object of study.
why it matters
This is the honest scoped $Z_{\mathrm{RS}}$ of Seven Gaps, Lane 2. Parent results proved from it include the modulus bounds $|Z|\le\sum\mu$ and $|Z|\le |\mathrm{BoundedComplex}, B|$, relabeling invariance under equivalence-preserving bijections, and the unitary case $w(K)=e^{i S(K)}$ (real action $S$) with $|w(K)|=1$, which yields the well-definedness statement for the scoped class.
In the broader Recognition stack it supplies a finite, measure-respecting path sum at fixed lattice scale, the combinatorial skeleton on which continuum or continuum-limit claims would later sit. It does not yet close the sharper exponential-growth semantics of growthBase for exact simplicial subclasses; that remains open. Framework contact is the gravity/path-sum side of the seven-gaps program rather than the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.