ShellSig
plain-language theorem explainer
A shell signature at level n is a triple (v, e, t) of vertex, edge, and triangle counts, each at most n, with the maximum exactly n. Packaging the counts in Fin(n+1) makes the signature type finite by construction. Anyone working the exact complexity shells or the CapShellBridge maps cites this type. It is a pure subtype abbreviation, not a proved statement.
Claim. For each $n \in \mathbb{N}$, a shell signature at level $n$ is a triple $(v,e,t)$ with $v,e,t \in \{0,\ldots,n\}$ satisfying $\max(v,e,t)=n$. Equivalently, it is the subtype of $\mathrm{Fin}(n+1)^3$ cut out by that max condition.
background
The module organizes quotient-class path-sum configuration space into exact complexity shells (no size caps in the shell definition) and studies the shell-resummed path sum with a hand-inserted Gaussian UV regulator $\exp(-\rho n^2)$. Honesty tags in the module doc stress that the regulator is mathematical, not derived physics, and that regulator removal ($\rho \to 0^+$) remains a named open.
A shell signature records the three combinatorial counts that index an exact complex: vertices $v$, edges $e$, and triangles $t$. The level $n$ is forced to be the complexity $\max(v,e,t)$, so each configuration sits in exactly one shell. Using $\mathrm{Fin}(n+1)$ for each coordinate makes the whole signature type finite, which is the prerequisite for Fintype instances on exact path classes and for cardinality bounds such as $\lvert\mathrm{ExactPathClass}, n\rvert \le (n+1)^{12(n+1)}$.
Upstream count and vertex abbreviations elsewhere in the monolith are ordinary cardinality or lattice-point types; here the triple is specialized to the exact-shell grading used by the Seven Gaps gravity path sum.
proof idea
Definitional abbreviation only: the type is the subtype of $\mathrm{Fin}(n+1)\times\mathrm{Fin}(n+1)\times\mathrm{Fin}(n+1)$ whose three natural-number coercions have maximum equal to $n$. No lemmas are applied; finiteness of the ambient product and the propositional max constraint are the entire content.
why it matters
This type is the index set for exact complexity shells. Downstream, exactComplexity reads complexity from the signature alone and records the no-double-counting fact that a complex sits in shell $n$ only when $n$ equals that complexity. ExactPathClass and the shell entropy bound exactPathClass_card_le quantify over these signatures.
The CapShellBridge layer uses shell signatures as the glue between cap-free exact complexes and bounded complexes: boundedShellSig extracts the signature of a bounded complex; exactToBounded, exactRelabelToBounded, and exactClassToCap thread a signature $s$ through the attach-cap and forget-cap maps; boundedToShell_exactToBounded shows the round trip recovers the original exact-shell class.
In the Recognition gravity stack this is Stage 1 scaffolding for the regulated path sum $Z_{\mathrm{RS}}^{\mathrm{uv}}$: finite shells plus the Gaussian weight give summability for every $\rho>0$. It does not touch continuum-limit or FullTheoryLedger flags, and it does not claim a physical action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.