shellSig_card_le
plain-language theorem explainer
At complexity level n, the number of admissible shell signatures (vertex/edge/tetrahedron count triples with max exactly n) is at most (n+1)^3. Gravity path-sum and shell-entropy arguments cite this as the signature-counting factor. The proof is a subtype-cardinality comparison against the ambient Fin(n+1)^3 cube, whose size is (n+1)^3 by product arithmetic.
Claim. For every natural number $n$, the number of shell signatures at level $n$ is at most $(n+1)^3$. A shell signature is a triple $(v,e,t)$ of natural numbers each at most $n$ with $\max(v,e,t)=n$.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells with no size caps in the shell definition, and studies a Gaussian-UV-regularized path sum. Complexity of a complex is the largest of its vertex, edge, and tetrahedron counts; that maximum is the shell coordinate.
A shell signature at level $n$ is a triple $(v,e,t)$ with each count in ${0,\ldots,n}$ and $\max(v,e,t)=n$. It is packaged as a subtype of $\mathrm{Fin}(n+1)^3$ so the type is finite by construction. The ambient cube has cardinality $(n+1)^3$; the signature set is the subset where the max-equals-$n$ predicate holds.
Stage 1 of the module builds shell structure (relabeling-invariant complexity, exact complexes, Fintype shells) before the regulated series estimates. This bound is the first counting step in that audit.
proof idea
Apply Fintype.card_subtype_le to the predicate $\max(v,e,t)=n$ on $\mathrm{Fin}(n+1)\times\mathrm{Fin}(n+1)\times\mathrm{Fin}(n+1)$. That gives $\lvert\mathrm{ShellSig},n\rvert\le\lvert\mathrm{Fin}(n+1)^3\rvert$. Then expand the product cardinality: each factor has size $n+1$, so the cube has size $(n+1)^3$ by Fintype.card_prod, Fintype.card_fin, and a one-line ring simplification. No deeper combinatorial enumeration is needed; the inequality is pure subtype-vs-ambient counting.
why it matters
This is the signature-counting half of the shell entropy bound (S1c). Downstream, exactPathClass_card_le multiplies $\le(n+1)^3$ signature choices by $\le(n+1)^{6(n+1)}$ labeled configurations per signature (via the quotient surjection from labeled exact complexes), then absorbs $3+6(n+1)\le 12(n+1)$ to get $\lvert\mathrm{ExactPathClass},n\rvert\le(n+1)^{12(n+1)}$. That entropy bound feeds the modulus estimate on regulated shell terms and the summability of the Gaussian-UV series for every $\rho>0$.
It also sits next to toExact_complexity, which identifies capped complexity with exact complexity on the image of the forget-cap map, so shell coordinates match across the bounded and exact presentations.
Framework role: Stage 1 scaffolding for the Seven Gaps path-sum program. The module is explicit that the regulator $\exp(-\rho n^2)$ is inserted by hand, the action/phase is a parameter, and regulator removal ($\rho\to 0^+$) remains a named open (HasZRSRegulatorRemoval). This lemma closes only the finite-signature count; it does not touch continuum limits or FullTheoryLedger flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.