shell_index_unique
plain-language theorem explainer
An exact combinatorial complex of signature (v,e,t) can belong to the complexity shell at level n only when n equals its exact complexity max(v,e,t). Anyone organizing the quotient path-sum into non-overlapping shells cites this uniqueness. The proof is a three-line rewrite: unfold the complexity, substitute the signature components, and apply the shell-max condition.
Claim. Let $K$ be an exact complex with exactly $v$ vertices, $e$ edges and $t$ tetrahedra. If a shell signature $s$ at level $n$ has components $(v,e,t)$, then necessarily $n$ equals the exact complexity of $K$ (i.e. $\max(v,e,t)$). Thus each exact configuration occupies exactly one complexity shell.
background
This module partitions the quotient-class path-sum configuration space into exact complexity shells and studies the Gaussian-UV-regularized shell series. An exact complex is a cap-free combinatorial type: incidence data for precisely $v$ vertices, $e$ edges and $t$ tetrahedra, with no size inequalities. Global equivalence is the relabeling relation on a fixed signature; different signatures cannot be equivalent because vertex/edge/tet bijections force equal cardinalities.
A shell signature at level $n$ is a triple $(v,e,t)$ with each count at most $n$ and $\max(v,e,t)=n$, packaged in finite types so each shell is finite. Exact complexity of a complex is that same maximum. The module's honesty protocol keeps the regulator $\exp(-\rho n^2)$ mathematical (not derived physics) and leaves regulator removal open.
proof idea
Term-mode, three steps. Unfold exactComplexity (definitionally $\max(v,e,t)$ for the complex). Rewrite the three signature projections using the hypotheses that the shell signature's vertex, edge and tet counts equal $v$, $e$ and $t$. The residual goal is exactly the defining property of a shell signature: $\max(v,e,t)=n$, which is the second component of the subtype, applied symmetrically.
why it matters
Without uniqueness, the same abstract complex could be counted in two shells, double-counting the path-sum measure. The doc-comment states the no-double-counting claim explicitly: combined with global equivalence living on a fixed signature, no complex appears in two shells. Downstream, the status structure ExactShellGaugeUVStatus lists this theorem among the Stage-1 shell-structure flags that ground shell_structure_proved. It is pure combinatorial bookkeeping for the seven-gaps gravity path sum; it does not touch continuum limits, physical actions, or the open regulator-removal flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.