tick_shift_excludes_fixed_point
plain-language theorem explainer
A shell automorphism that advances every exact-path class by one Fin-8 tick cannot fix any class: fixed point plus +1 rotation forces τ(c)=τ(c)+1 in Fin 8, which is impossible. Gravity/Gap2 authors cite it to kill candidate TailFiberShift witnesses that fix a class in each shell. The proof is a three-line rewrite into the sibling lemma that x+1≠x on Fin 8.
Claim. Let $\tau_n$ assign to each exact-path class at shell $n$ a tick in $\mathrm{Fin}\,8$, and let $\sigma$ be a bijection on those classes such that $\tau_n(\sigma(c))=\tau_n(c)+1$ for every class $c$. Then $\sigma$ has no fixed point: $\sigma(c)=c$ is contradictory.
background
The module banks a conditional bridge for residual R4 of the enriched-carrier phase route in Gap2. The structure hypothesis TailFiberShift asks for a tail family of class-preserving shell automorphisms that rotate the Fin-8 tick label by $+1$. Existence of such a free action is left open; the module instead records consequences and no-gos.
Exact-path classes are the equivalence classes of exact complexes at shell level $n$. The tick map $\tau_n$ lands in $\mathrm{Fin},8$, the eight-tick octave forced by the Recognition chain (T7). The sibling lemma fin8_add_one_ne states that adding one is never the identity on $\mathrm{Fin},8$.
Candidate geometric operations (endpoint reversal, tetrahedron slot rotation, their composite) each fix a degenerate labeled complex in every shell, so their induced class maps fix a class. That is the setting in which a fixed-point exclusion becomes a no-go against the tick-shift field.
proof idea
Term-mode contradiction in three steps. Instantiate the tick-shift hypothesis at the putative fixed class $c$ to get $\tau_n(\sigma c)=\tau_n(c)+1$. Rewrite the left side with $\sigma c=c$, yielding $\tau_n(c)=\tau_n(c)+1$. Discharge by the sibling fin8_add_one_ne applied to $\tau_n(c)$ (after symmetry of the equality). No other lemmas are needed.
why it matters
Feeds the immediate parent fixed_class_blocks_tick_shift, which lifts the single-shell exclusion to a tail: any candidate shift family that fixes a class in every shell $n\ge N$ cannot satisfy the tick-shift field of TailFiberShift.
In the Recognition Gravity Gap2 ledger this is fallback credit on residual R4. The eight-tick octave (T7) makes $+1$ on $\mathrm{Fin},8$ free of fixed points, so geometric candidates that fix degenerate complexes (endpoint reversal, tet slot rotation) are ruled out as TailFiberShift witnesses. R4 itself stays open and uninhabited; gap2_continuum_and_measure remains false. Signature-level Fin-8 oscillatory routes stay closed by the separate Burnside stall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.