fixed_class_blocks_tick_shift
plain-language theorem explainer
A tail family of exact-path-class automorphisms that fixes some class in every shell cannot also advance the Fin-8 tick label by one. Gap2 / enriched-carrier workers cite this as the abstract obstruction behind the labeled-operation no-gos. The proof specializes the fixed-point exclusion lemma at the base shell N.
Claim. Let $\tau_n$ assign each exact path class at shell $n$ a value in $\mathrm{Fin}\,8$. Suppose from shell $N$ onward there are bijections $s_n$ on exact path classes such that every $s_n$ has a fixed class, and $\tau_n(s_n(c))=\tau_n(c)+1$ for all classes $c$. Then a contradiction follows.
background
This module banks a conditional bridge for residual R4 of the Gap2 enriched-carrier phase. The structure hypothesis TailFiberShift asks for a tail family of exact-path-class automorphisms that preserve the mass functional classMu and rotate a Fin-8 tick assignment $\tau$ by $+1$. Existence of such a free action is left open; the module instead records consequences and candidate no-gos.
Exact path classes live on successive shells indexed by $n\in\mathbb{N}$. The tick lands in $\mathrm{Fin},8$, matching the eight-tick octave forced at T7 of the unified forcing chain. A fixed class for a candidate shift means some class $c$ with $s_n(c)=c$; the tick-shift field would then require $\tau_n(c)=\tau_n(c)+1$ in $\mathrm{Fin},8$, which is impossible.
The sibling lemma tick_shift_excludes_fixed_point packages that local incompatibility. The present theorem lifts it to a uniform tail statement: fixed classes in every shell block any candidate that tries to satisfy the tick-shift axiom of TailFiberShift.
proof idea
Term-mode, two steps. Instantiate the fixed-class hypothesis at the base shell $N$ (with $N\le N$) to obtain a concrete fixed class $c$ for $s_N$. Feed the tick-shift hypothesis at that same shell, together with the fixed-point equation, into the sibling tick_shift_excludes_fixed_point, which already shows that $\tau(s(c))=\tau(c)+1$ rules out $s(c)=c$. The resulting False discharges the goal.
why it matters
This is the shared abstract engine for the three labeled no-gos in the same module: endpoint reversal, tetrahedron slot rotation, and their composite each fix a degenerate class in every shell, so none can supply a TailFiberShift. Downstream docs state the obstruction directly: fixed classes are "incompatible with tick_shift".
In the Recognition framework the Fin-8 tick is the T7 eight-tick octave; any continuum/measure route that needs an oscillatory tail via a free tick-rotating action must therefore avoid fixed classes. Residual R4 stays open (uninhabited free action), and gap2_continuum_and_measure remains false. Signature-level Fin-8 routes are separately stalled by the Burnside blocker; this theorem closes the obvious geometric candidates on labeled exact complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.