sigV
plain-language theorem explainer
Extracts the vertex count from a shell signature at complexity level n. Anyone working with exact path classes, shell measures, or the cap–shell bridge cites this projection. The body is a one-line field projection from the Fin-packaged triple (v,e,t).
Claim. Given a shell signature $s=(v,e,t)$ at level $n$ (each of $v,e,t$ is in $\{0,\ldots,n\}$ and $\max(v,e,t)=n$), the vertex count is the first coordinate: $\mathrm{sigV}(s)=v\in\mathbb{N}$.
background
This module builds exact complexity shells for the quotient-class path-sum configuration space, with no size caps in the shell definition, and proves Gaussian-UV-regularized shell series converge for every $\rho>0$. The regulator and action are mathematical parameters; continuum removal stays open.
A shell signature at level $n$ is a triple $(v,e,t)$ of counts in $\mathrm{Fin}(n+1)$ with $\max(v,e,t)=n$, so the signature type is finite. Exact complexes and their global-relabeling quotients are indexed by these signatures. The three projections (vertex, edge, triangle counts) unpack the triple for use in ExactComplex, setoids, and measures.
Sibling projections supply edge and triangle counts the same way. Downstream, exact path classes are dependent sums over signatures of those quotients.
proof idea
One-line abbrev: coerce the first $\mathrm{Fin}(n+1)$ component of the underlying product triple to $\mathbb{N}$. No lemmas, no tactics.
why it matters
This is the vertex leg of the shell signature API. Exact path classes are defined as $\Sigma_{s:\mathrm{ShellSig},n},Q(\mathrm{exactSetoid}(\mathrm{sigV},s,\mathrm{sigE},s,\mathrm{sigT},s))$, so every shell element carries its vertex count through this projection. The per-class measure classMu and the cardinality bound on exact path classes both route through it.
On the bridge side, exactToBounded, exactRelabelToBounded, exactClassToCap, and boundedToShell_exactToBounded attach or forget caps using sigV s as nV. Without a stable vertex projection, the exact-to-bounded comparison and the shell-resummed UV path sum cannot be stated.
It sits in Stage 1 shell structure of the Seven Gaps gravity stack: combinatorial bookkeeping only, not continuum physics. It does not touch regulator removal or any FullTheoryLedger flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.