Zsimp
plain-language theorem explainer
Defines the path sum over only the simplicial subclass of bound-B incidence configurations, using the same 1/|Aut| measure and complex weight as the unrestricted sum. Gravity and SevenGaps path-sum arguments cite it as the UV-safe restricted partition function. The body is a finite sum over the Fintype of simplicial complexes.
Claim. For a bound $B\in\mathbb{N}$ and a weight $w$ on bounded incidence configurations, the simplicial path sum is $Z_{\mathrm{simp}}(B,w)=\sum_{K\in\mathcal{S}_B}\mu(K)\,w(K)$, where $\mathcal{S}_B$ is the simplicial subclass of bound-$B$ complexes and $\mu$ is the $1/|\mathrm{Aut}|$ configuration measure.
background
In the SevenGaps path-sum setup, BoundedComplex B is the garbage-inclusive superclass of bounded incidence configurations: every combinatorial triangulation of bound $B$, plus degenerate edges, multi-edges, repeated tet vertices, and tets whose 1-skeleton is incomplete. This module carves out the true simplicial subclass via four combinatorial conditions: no degenerate edges, no multi-edges, four distinct tet vertices, and skeleton closure (every tet vertex pair appears as an edge).
The unrestricted path sum $Z$ sums $\mu(K)w(K)$ over all bounded complexes. Here $\mu$ is the same $1/|\mathrm{Aut}|$ measure used for $Z$; $w$ is an arbitrary complex-valued weight on configurations. The simplicial subclass is a Fintype of strictly positive cardinality (witnessed by the single tetrahedron with full 1-skeleton), so the restricted sum is a well-defined finite sum in $\mathbb{C}$.
Face (triangle) data is not carried by the incidence shape, so triangle closure is out of scope; that honesty is recorded in the module status note.
proof idea
Definition, not a theorem. The body is the finite sum of $(\mu(K):\mathbb{C})\cdot w(K)$ as $K$ runs over the Fintype of simplicial complexes of bound $B$. Noncomputable only because the ambient complex arithmetic and measure live in $\mathbb{C}$/$\mathbb{R}$; no axioms or sorry.
why it matters
Phase 0b of the full gravity path-sum theory needs a UV-safe configuration class before any continuum or continuum-limit claim. Restricting to the simplicial subclass removes degenerate and multi-edge garbage that would spoil measure bounds.
The sole immediate consumer is the UV-finiteness theorem: for unit-modulus weights, the norm of this restricted sum is at most the simplicial configuration count. That bound is the combinatorial half of showing the simplicial path sum does not diverge as a pure counting artifact. Downstream gravity arguments that quote a finite simplicial partition function land on this definition first.
It does not itself close continuum limits or identify physical 3-geometry; it only supplies the restricted summand class demanded by the SevenGaps finiteness chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.