sigmaTick_is_ShellSigTick
plain-language theorem explainer
Any Fin-8 coloring of shell signatures induces a tick assignment on exact path classes that factors purely through the signature triple. Gravity-gap workers cite this when packaging signature-only tick maps into the signature-factoring tick predicate. The proof is a one-line existential package discharged by definitional equality.
Claim. For every family of maps $\sigma_n$ sending shell signatures at level $n$ into $\mathrm{Fin}\,8$, the induced tick assignment $\tau_n(c)=\sigma_n(\mathrm{sig}(c))$ on exact path classes factors through shell signatures: there exists a signature coloring realizing $\tau$.
background
In the Gap-2 continuum attack, exact path classes at shell level $n$ carry a shell signature $(v,e,t)$: a triple of counts in $\mathrm{Fin}(n+1)$ whose maximum equals $n$. A tick assignment maps path classes to $\mathrm{Fin},8$. The signature-factoring tick predicate isolates assignments that ignore quotient-internal incidence data and depend only on that triple.
The packaging map turns a signature coloring into a tick assignment by evaluating the coloring on the class signature. Upstream, shell signatures are finite subtypes of count triples; the factoring predicate is the existential statement that some coloring reproduces the tick on every class.
This module is the Wave C1 R4 terminal attack on the oscillatory-tail blocker. After single-signature mass concentration fails for large shells (cube dominance only mesoscopic), the remaining route studies Fin-8 cancellation under signature-factoring ticks, packaged against Burnside mass identities.
proof idea
Term-mode existential introduction. The witness is the given signature coloring itself. The pointwise equality obligation (induced tick on a class equals the coloring on its signature) holds by definition of the packaging map and is discharged by rfl. No lemmas are applied.
why it matters
Feeds the biconditional that identifies the signature-factoring tick predicate with existence of a packaged coloring, and the honest reformulation of the Fin-8 oscillatory-tail blocker as an explicit signature-mass cancellation statement. The latter parent applies this theorem when lifting a coloring-plus-tail hypothesis into the blocker Prop:
hblocker ⟨sigmaTick sigma, sigmaTick_is_ShellSigTick sigma, htail⟩.
Those parents convert the blocker into a form attackable with Burnside mass lemmas (signatureMass_eq_burnside, shell-mass summation, fiberwise amplitude grouping). The module lands reduction and stall diagnosis only: it does not flip gap2_continuum_and_measure. Route (a)/(b) single-signature concentration is already refuted as a uniform asymptotic strategy; this packaging keeps the signature-only attack channel well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.