shellSig_zero_eq
plain-language theorem explainer
At shell level 0 every admissible signature equals the isolated triple (0,0,0). Gravity and QG residual arguments cite this to pin the empty-complex class as the unique base-shell representative. The proof is a short subtype-and-product extensionality argument using that Fin 1 is a singleton.
Claim. Every shell signature $s$ at level $0$ equals the isolated signature $(0,0,0)$. Equivalently, if $s=(v,e,t)$ with $v,e,t\in\mathrm{Fin}\,1$ and $\max(v,\max(e,t))=0$, then $s$ is definitionally the unique such triple.
background
A shell signature at level $n$ is a triple $(v,e,t)$ of vertex, edge, and triangle counts, each packaged in $\mathrm{Fin}(n+1)$ so that $\max(v,\max(e,t))=n$. The type is therefore finite. The isolated signature at level $n$ is the concrete point $(n,0,0)$, the $n$-isolated-vertices complex.
At $n=0$ the ambient product is $\mathrm{Fin},1\times\mathrm{Fin},1\times\mathrm{Fin},1$, whose only element is $(0,0,0)$, and the max constraint is automatic. Thus the subtype collapses to a singleton.
This module hardens the R4 residual in the Gap-2 tick-phase tail blocker: shell $0$ being a singleton class forces class-mass to concentrate in one tick fiber, blocking all-shell mass balance at the finite head.
proof idea
Apply subtype extensionality to drop the max-constraint proof component, then product extensionality twice on the triple. Each coordinate lives in $\mathrm{Fin},1$, so $\mathrm{Fin.eq_zero}$ identifies it with $0$. The resulting triple is definitionally $\mathrm{isolatedSig},0$.
why it matters
Feeds $\mathrm{exactPathClass_zero_eq}$, which lifts the uniqueness from signatures to exact path classes at shell $0$ ("every class at shell $0$ equals the unique empty-complex class"). That fact is the finite-head half of the R4 hardening: because shell $0$ is a singleton, $\mathrm{classMu}$-mass cannot be balanced across tick fibers for any $\tau$, so $\neg\exists\tau,,\mathrm{TickFiberMassBalanced},\tau$. The eventual-balance repair then kills late amplitudes independently of the head. The broader open target remains existence of a substrate phase with oscillatory tail (and the defined but unproved $\mathrm{SignatureFin8OscillatoryTailBlocker}$); this lemma only closes the base-shell uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.