instNonemptyExactPathClass
plain-language theorem explainer
Every exact complexity shell is inhabited: for each natural number n there is at least one combinatorially distinct exact complex of complexity exactly n. The witness is the n-isolated-vertices complex. Anyone citing shell support for the Gaussian-UV path sum, or the Stage-1 unbounded-support claim (S1d), would use this. One-line instance that packages the isolated-class constructor as a Nonempty proof.
Claim. For every $n \in \mathbb{N}$, the exact complexity shell of level $n$ is nonempty: there exists at least one global-equivalence class of exact labeled complexes whose complexity (max of vertex, edge, and tetrahedron counts) equals $n$.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells with no size caps, then studies the shell-resummed path sum with a hand-inserted Gaussian UV regulator $\exp(-\rho n^2)$. Complexity of a complex is the max of its vertex, edge, and tetrahedron counts; that integer is the shell coordinate.
The exact complexity shell ExactPathClass n is the disjoint union, over shell signatures of total complexity $n$, of the quotient of exact labeled complexes by global relabeling equivalence. No bounded-complex cap type appears in the definition.
The module's Stage-1 list records that every shell is inhabited, with witness the complex of $n$ isolated vertices and with an explicit disclaimer of no simpliciality claim. The present instance is the typeclass form of that inhabitation fact.
proof idea
One-line instance: the term is the pair constructor for Nonempty, applied to isolatedClass n. That constructor supplies a concrete point of ExactPathClass n (the class of the $n$-isolated-vertices exact complex), which is enough to inhabit the type. No further lemmas or tactics are needed.
why it matters
This is the typeclass packaging of Stage-1 claim S1d (unbounded support): no shell is eventually empty. Without it, the shell-indexed series for the regulated path sum $Z_{\mathrm{RS}}^{\mathrm{UV}}$ could in principle skip levels; with it, every $n$ contributes a nonempty finite set of classes (finiteness is the sibling Fintype instance).
It sits inside the honesty boundary of the module: the regulator is mathematical, not derived physics; regulator removal remains a named open; nothing here is the continuum limit or a FullTheoryLedger flip. Downstream used-by edges are empty in the graph snapshot, so the immediate consumers are the shell-summability and cutoff-convergence theorems in the same module rather than external parents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.