ShellSigTick
plain-language theorem explainer
A Fin-8 tick assignment on exact path classes is a shell-signature tick when it factors through the shell triple alone, ignoring quotient-internal incidence. Downstream Gap2 phase-close and enriched-carrier packages treat this class as a named decoy to exclude. The body is a pure existential Prop definition, not a proved claim.
Claim. A tick assignment $\tau$ (sending each exact path class at shell $n$ to an element of $\mathrm{Fin}\,8$) is a shell-signature tick if there exists $\sigma$ depending only on the shell signature $(v,e,t)$ such that $\tau_n(c)=\sigma_n(\mathrm{sig}(c))$ for every $n$ and every exact path class $c$.
background
This module hardens the R4 residual in the Gap2 continuum/measure campaign after the R2 cross-family correction. The eight-tick octave (period $2^3$) supplies the $\mathrm{Fin},8$ phase labels; a tick assignment colors every exact path class by one of those eight values. Shell signature means the coarse triple $(v,e,t)$ of a class, with no internal incidence data from the path quotient.
The local setting distinguishes several dead or insufficient routes to an oscillatory tail: all-shell fiber-mass balance forces every exact shell amplitude to vanish (hence contiguous-block cancellation), but shell $0$ is a singleton so global mass balance is impossible; eventual balance repairs the finite head. Signature-only colorings are the remaining named decoy class.
Upstream, tick is the RS-native time quantum $\tau_0=1$, and the eight-tick structure is the fundamental evolution period tied to the Clifford/Bott grading. Exact path classes and shell signatures live in the Gap2 tick-phase substrate imported by this module.
proof idea
Definitional, not a proof. The Prop is the existential statement that some shell-signature-only map $\sigma$ agrees with $\tau$ on every class via the signature projection $c\mapsto c.1$. No tactics, no lemmas applied; inhabitation or refutation is deferred to downstream theorems that construct or exclude particular $\tau$.
why it matters
Marks the signature-only decoy inside the sharpened R4/R5 attack surface. CertifiedGap2Fin8PhaseClose requires a named tick recipe whose derived phase is not shell-constant, not eventually zero, and not a shell-signature tick. EnrichedCarrierPhaseSubstrate and TypedResidual_enriched_carrier_oscillatoryTail demand a global-equivalent-invariant labeled tick whose descent has an oscillatory tail and is not a shell-signature tick.
The theorem selfLoopClassTick_not_ShellSigTick shows the self-loop recipe uses quotient-internal incidence and therefore escapes this class. The iff signatureBlocker_iff_no_shellSig_oscillatoryTail identifies the terminal blocker with: no shell-signature tick yields an oscillatory tail on the derived phase. That blocker is defined, neither proved nor assumed; the R4 residual (a substrate phase with oscillatory tail outside dead classes) stays open. Does not flip gap2_continuum_and_measure. Framework landmark: eight-tick octave (T7) as the $\mathrm{Fin},8$ phase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.