complexity
plain-language theorem explainer
Complexity of a size-bounded simplicial complex is the maximum of its vertex, edge, and tetrahedron counts, used as the discrete shell coordinate in the seven-gaps path-sum setup. Anyone working on exact shells, shell entropy bounds, or the Gaussian-UV regulated series cites this. The definition is a direct three-way max on the count fields.
Claim. For a natural bound $B$ and a $B$-bounded complex $K$, the complexity of $K$ is $\max\{n_V(K),\, n_E(K),\, n_T(K)\}$, where $n_V$, $n_E$, and $n_T$ are the numbers of vertices, edges, and tetrahedra. This integer is the shell coordinate.
background
The module builds exact complexity shells for the quotient-class path-sum configuration space of 3D simplicial complexes, then studies a Gaussian UV-regulated shell series $\exp(-\rho, n^2)$. Honesty tags in the module state that the regulator is inserted by hand, the phase is a free class-invariant parameter, and regulator removal ($\rho\to 0^+$) remains an open named hypothesis.
A bounded complex (from the path-sum measure layer) carries finite vertex, edge, and tetrahedron counts under a size bound $B$. Complexity collapses those three counts to a single natural number: the largest of them. That number indexes the exact shell of complexes of complexity $n$, without imposing a separate size cap inside the shell definition itself.
Downstream shell structure treats this coordinate as relabeling-invariant and uses it to form finite exact path classes, entropy bounds of the form $\lvert\mathrm{ExactPathClass}, n\rvert\le (n+1)^{12(n+1)}$, and the regulated shell terms of the UV path sum.
proof idea
Pure definition: return $\max(n_V,\max(n_E,n_T))$ on the three count fields of the bounded complex. No lemmas, no tactics.
why it matters
This is the Stage-1 shell coordinate for the seven-gaps exact-shell program. The module proves it is invariant under relabeling, then builds the cap-free exact class, the exact path-class fintype, the shell entropy bound, and inhabited shells (including the $n$-isolated-vertex witness). Those shells feed the modulus bound on regulated shell terms, summability for every $\rho>0$, and convergence of cutoff partial sums to the UV path sum $Z_{\mathrm{RS}}^{\mathrm{uv}}$.
It does not flip continuum or FullTheoryLedger flags: complexity cutoffs are not mesh refinement, and regulator removal stays open. In the broader Recognition gravity stack it is the discrete size index against which path-class measures $1/\lvert\mathrm{Aut}\rvert$ and Gaussian damping are organized, not a derived continuum length.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.