sigT
plain-language theorem explainer
Extracts the tetrahedron count from a shell signature at complexity level n. Anyone assembling ExactPathClass, class measures, or the CapShellBridge maps cites this projection. The body is a one-line field access on the Fin-packaged triple (v,e,t).
Claim. Given a shell signature $s=(v,e,t)$ at level $n$ (each of $v,e,t\in\{0,\ldots,n\}$ with $\max(v,e,t)=n$), the tetrahedron count is $t\in\mathbb{N}$.
background
This module organizes the 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: the regulator is mathematical, not derived physics; regulator removal $\rho\to 0^+$ remains a named open.
A shell signature at level $n$ is a triple $(v,e,t)$ of vertex, edge, and tetrahedron counts, each at most $n$, with $\max(v,e,t)=n$. It is packaged as a subtype of $\mathrm{Fin}(n+1)^3$ so the signature type is finite. Sibling projections give the vertex and edge counts; this declaration is the tetrahedron leg.
The exact complexity shell is the disjoint union, over all such signatures, of labeled exact complexes of those counts modulo global relabeling. No bounded-cap type appears in that definition.
proof idea
Definitional abbreviation: unpack the subtype carrier (a triple in $\mathrm{Fin}(n+1)^3$) and cast the third component to $\mathbb{N}$. No lemma applications.
why it matters
Feeds every construction that needs the tetrahedron dimension of an exact shell. Downstream, ExactPathClass is $\Sigma_{s:\mathrm{ShellSig},n}$ of the quotient at $(\mathrm{sigV},s,\mathrm{sigE},s,\mathrm{sigT},s)$; classMu evaluates the per-class measure on those counts; exactPathClass_card_le and shell_index_unique quantify over signatures via the same projections.
On the bridge side, exactToBounded, exactRelabelToBounded, exactClassToCap, and boundedToShell_exactToBounded attach or forget a complexity cap $B\ge n$ while preserving incidence data keyed by these three counts. Without the tetrahedron projection the exact-to-bounded dictionary cannot typecheck.
In the Seven Gaps program this is Stage-1 shell structure scaffolding only: it supports the Fintype and entropy bound on exact shells, not continuum limits or FullTheoryLedger flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.