ShellSigTick_iff_sigmaTick
plain-language theorem explainer
A Fin-8 tick on exact path classes of complexity n is signature-constant exactly when it factors through a map on shell signatures. Analysts packaging the Fin-8 oscillatory-tail blocker for Gap 2 cite this equivalence to swap between path-class and signature-level witnesses. The proof is a two-line constructor: reassociate the existential witness one way, apply the companion lift lemma the other.
Claim. Let $\tau$ assign to every exact path class of complexity $n$ a value in $\mathrm{Fin}\,8$. Then $\tau$ is a shell-signature tick if and only if there exists a family $\sigma_n$ of maps from shell signatures of complexity $n$ into $\mathrm{Fin}\,8$ such that $\tau$ equals the canonical lift of $\sigma$ through the signature projection on exact path classes.
background
Exact path classes of complexity $n$ are the combinatorially distinct exact complexes at that shell: the disjoint union, over shell signatures, of the quotient of the exact labeled class by global equivalence. No bounded-complex cap appears in the definition. Shell signatures record the combinatorial type $(v,e,t)$ at fixed complexity.
The target $\mathrm{Fin},8$ is the eight-tick octave (period $2^3$), the fundamental RS evolution period. A shell-signature tick is a path-class assignment that is constant on fibers of the signature projection. The companion constructor lifts any signature-level $\mathrm{Fin},8$ map to such a path-class tick.
Local setting is the Wave C1 R4 terminal attack on the Fin-8 oscillatory-tail blocker in the seven-gaps gravity stack. The blocker Prop itself is not proved; landed material packages Burnside signature masses, shell-mass decompositions, and honest reformulations of the blocker as an explicit sequence statement.
proof idea
Iff by constructor. Left to right: unpack the shell-signature-tick witness $(\sigma,h)$, re-export $\sigma$, and discharge functional equality by funext on $(n,c)$, applying $h$ pointwise. Right to left: given $\tau$ definitionally equal to the canonical lift of $\sigma$, apply the companion lemma that every such lift is a shell-signature tick.
why it matters
Direct input to the parent equivalence that rewrites the Fin-8 oscillatory-tail blocker as an explicit signature-mass cancellation statement. That parent turns a shell-signature-tick hypothesis into a signature-level witness by composing this packaging with the lift lemma, then feeds the tail hypothesis through.
In the seven-gaps program this is infrastructure on the Gap 2 continuum-and-measure line, not a discharge of it. Module status is explicit: single-signature mass concentration fails as a uniform large-$n$ strategy (cube dominance only mesoscopic; by $n\approx 400$ the top signature is below $1/8$ of shell mass), and the $>1/8$ fiber-balance obstruction likewise fails asymptotically. The eight-tick octave (T7) is the phase target being cancelled; nothing here touches T5 J-uniqueness, phi-forcing, or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.