BoundedComplex
plain-language theorem explainer
A size-capped combinatorial 3-complex: at most B vertices, edges, and tetrahedra, with abstract edge and tet incidence maps and no metric field. Gravity and path-sum workers cite it as the scoped configuration class for the finite Z_RS measure. It is a pure structure definition mirroring Regge/CDT incidence with an explicit bound B.
Claim. For each natural number $B$, a bounded complex consists of counts $n_V,n_E,n_T\le B$ together with incidence maps $E\colon\{0,\ldots,n_E-1\}\to\{0,\ldots,n_V-1\}^2$ and $T\colon\{0,\ldots,n_T-1\}\to\{0,\ldots,3\}\to\{0,\ldots,n_V-1\}$. Configurations are combinatorial and equilateral at fixed lattice scale (metric data dropped).
background
Lane 2 of the Seven Gaps campaign builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of 3D triangulations. The recognition substrate fixes edge length at the minimum mesh, so configurations are combinatorial and equilateral in the CDT style: all geometric content sits in incidence data.
BoundedComplex B is that scoped class. It copies the incidence shape of Triangulation3D (vertex/edge/tet counts, edge endpoint pairs, four vertices per tet) but drops the metric field and adds explicit size caps $n_V,n_E,n_T\le B$. Upstream Freudenthal cube and two-cube-strip tables supply concrete edge and tet vertex lists of this same shape; the polarized-birth interface and rung-descent edge-vertex extractors are related combinatorial edge data, not prerequisites of the structure itself.
The module's honesty note: the structure admits arbitrary bounded incidence, so it contains all bounded triangulations and also non-simplicial configurations. Finiteness of this superclass still yields finiteness of every subclass used later.
proof idea
No proof body: this is a structure declaration. Fields package three natural counts, three inequality witnesses against the cap $B$, an edge-endpoint map on Fin nE, and a tet-vertex map on Fin nT \times Fin 4. Downstream code treats inhabitants as labeled complexes; emptiness is witnessed separately by emptyComplex.
why it matters
This is the configuration type on which the whole Lane-2 path-sum stack sits. The module proves the class is a Fintype (via an explicit code equivalence), that relabeling is an equivalence relation with finite quotient, that automorphism groups are finite so the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ lies in $(0,1]$, and that $Z(B,w)=\sum_K \mu(K),w(K)$ is a finite, relabel-invariant sum with norm bounds—including the unitary weights $w=e^{iS}$.
Downstream, CapShellBridge forgets the cap proofs (toExact, boundedToShell, shell index/signature) and equates bounded and exact automorphism cardinalities, so measures agree under cap forgetting. CampaignLedger.campaign_flags_anchored re-derives load-bearing gap results from imported artifacts; this type is part of that anchored gravity stack.
Framework role: discharges the count-finiteness content of the postulated growthBase field in PathSumUVBound.AdmissibleTriangulationFamily. Sharper exponential-growth semantics for exact simplicial subclasses remains open. Landmark contact is the gravity/path-sum side of RS, not T0–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.