exactPathClass_unbounded_support
plain-language theorem explainer
Every exact complexity shell is nonempty: for each natural number n there exists at least one global-relabeling class of exact labeled complexes with complexity exactly n. Path-sum and shell-resummation arguments in the Seven Gaps gravity stack cite this to guarantee unbounded support of the shell series. The proof is a one-line appeal to positivity of finite cardinality once nonemptiness of the shell type is in hand (witness: n isolated vertices).
Claim. For every natural number $n$, the exact complexity shell at level $n$ is inhabited: $0 < \#(\text{exact complexes of complexity }n)/\sim$, where $\sim$ denotes global relabeling equivalence on exact labeled complexes.
background
The ambient module organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps in the shell definition) and studies a Gaussian-UV-regularized path sum $\exp(-\rho\cdot n^2)$. An exact complexity shell at level $n$ is the disjoint union, over shell signatures of complexity $n$, of the quotient of the exact labeled class by the global-equivalence setoid. No bounded-complex cap type enters that definition.
Complexity is a combinatorial size functional on labeled complexes and is invariant under relabeling. Stage 1 of the module proves shells are finite types, gives an entropy bound on their cardinality, and asserts every shell is inhabited. The inhabitance witness is the complex of $n$ isolated vertices (complexity exactly $n$); the module doc explicitly disclaims any simpliciality claim on that witness.
proof idea
One-line term proof: apply Nat.card_pos. That lemma reduces $0 < \mathrm{Nat.card},\alpha$ to Nonempty $\alpha$. Nonemptiness of the exact shell type is already supplied by the shell construction, via the $n$-isolated-vertices representative. No further combinatorial casework appears in the body.
why it matters
This is Stage-1 theorem S1d (unbounded support) in the exact-shell Gaussian-UV module: no shell is eventually empty, so the shell series is genuinely infinite. The grounding theorem exactShellGaugeUVStatus_grounded ties the shell_structure_proved status flag to the kernel statement $\forall n,,0<\mathrm{Nat.card}(\mathrm{ExactPathClass},n)$, of which this is the pointwise form.
Without unbounded support the regulated path sum could collapse to a finite sum; with it, the hand-inserted Gaussian regulator must control an infinite series for every $\rho>0$. The module's honesty disclosures still apply: regulator removal ($\rho\to 0^+$), physical action/phase, and continuum/mesh limits remain open and are not advanced here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.