isolatedVertices
plain-language theorem explainer
The n-point discrete complex with empty edge and tetrahedron incidence: exactly n vertices and nothing else. Complexity is n, and it is the canonical witness that every exact complexity shell is inhabited. Downstream Gap-2 and shell-class constructions cite it as the zero-incidence base case; the construction is immediate from empty Fin maps.
Claim. For each $n \in \mathbb{N}$, there is an exact combinatorial complex with signature $(v,e,t)=(n,0,0)$: the edge-incidence map $\mathrm{Fin}\,0 \to \mathrm{Fin}\,n \times \mathrm{Fin}\,n$ and the tetrahedron-incidence map $\mathrm{Fin}\,0 \to (\mathrm{Fin}\,4 \to \mathrm{Fin}\,n)$ are the unique empty maps. No simpliciality hypothesis is imposed.
background
The ambient module builds exact complexity shells for the quotient-class path-sum configuration space and proves Gaussian-UV-regularized shell series converge for every regulator strength $\rho>0$. Honesty constraints are binding: the regulator $\exp(-\rho n^2)$ is inserted by hand, the phase is a free class function, and regulator removal remains a named open.
An exact complex of signature $(v,e,t)$ is a cap-free triple of incidence data: edge endpoints $\mathrm{Fin},e\to\mathrm{Fin},v\times\mathrm{Fin},v$ and tet vertices $\mathrm{Fin},t\to(\mathrm{Fin},4\to\mathrm{Fin},v)$, with no size inequalities. Complexity is the integer $v+e+t$; shells group complexes by that integer up to independent relabeling.
Empty index types $\mathrm{Fin},0$ supply unique maps out of the empty set. The $n$-isolated-vertices object is the pure discrete point set of cardinality $n$ inside this language: complexity exactly $n$, used as the shell-inhabitation witness with no claim that the complex is a simplicial complex.
proof idea
Definitional construction, not a proof. Fill the two incidence fields of ExactComplex n 0 0 by the unique functions out of Fin 0, written fun i => i.elim0 for both edge and tet data. No lemmas are applied; emptiness of the domain discharges both fields.
why it matters
Stage 1 of the module lists every exact shell as inhabited, with witness "$n$ isolated vertices — NO simpliciality claim." This definition is that witness; isolatedClass packages it as the shell class at level $n$.
Gap-2 bridges use it as the fixed point of endpoint reversal and tet-slot rotation (both operations act only on edges or tets, hence fix the empty-incidence complex). The zero-signature uniqueness lemma identifies every ExactComplex 0 0 0 with the $n=0$ case. A posting-phase non-factorization argument instantiates the same zero complex as a counterexample carrier.
In the Seven Gaps gravity stack this is scaffolding for shell entropy and regulated path sums, not continuum physics: it does not touch T0–T8 forcing, RCL, or the $\alpha$ band, and it flips no continuum-limit ledger flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.