isolatedClass
plain-language theorem explainer
The canonical witness that every exact complexity shell is inhabited: the equivalence class of n isolated vertices (no edges, no tetrahedra). Gravity and path-sum arguments cite it to prove shells are nonempty and to pin shell-constant phases. Construction is a pair: the shell signature (n,0,0) with the quotient class of that labeled complex.
Claim. For each $n \in \mathbb{N}$, the pair consisting of the shell signature $(n,0,0)$ and the global-equivalence class of the labeled complex with $n$ vertices, zero edges, and zero tetrahedra is an element of the exact complexity shell at level $n$.
background
This module builds exact complexity shells for the Recognition path-sum configuration space: no size caps, only combinatorial type. Complexity is the max of vertex, edge, and tetrahedron counts. An exact complexity shell at level $n$ is the disjoint union, over shell signatures of complexity exactly $n$, of labeled exact complexes quotiented by global relabeling equivalence.
The $n$-isolated-vertices complex has $n$ vertices and empty edge and tetrahedron data, so complexity exactly $n$. Its signature $(n,0,0)$ is a valid shell signature because $\max(n,0,0)=n$. No simpliciality is claimed or required; the object is only a combinatorial witness that the shell is nonempty.
The module is explicit that the Gaussian UV factor $\exp(-\rho n^2)$ is a hand-inserted mathematical regulator, not derived physics, and that regulator removal remains open.
proof idea
One-line definitional pair. First component is the shell signature $(n,0,0)$. Second is the quotient class of the labeled $n$-isolated-vertices complex under the exact global-equivalence setoid. No tactics or lemmas beyond the constructors of those two upstream definitions.
why it matters
This is the Stage-1 unbounded-support witness: every shell is inhabited, so the shell series has no eventual empty terms. It discharges the Nonempty instance on each exact path class and feeds the shell-mass positivity argument (sum of positive per-class measures over a nonempty finite type).
Downstream, shell-constant phases are defined by equality to the phase on this class, and the shell-amplitude identity for constant phase factors out shell mass times a single unit phase evaluated here, ruling out intra-shell cancellation. That sits inside the Seven Gaps gravity path-sum stack; 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.