shiftBucketEquiv
plain-language theorem explainer
Under a tail antipodal shift, the mu-preserving tick shift induces a self-bijection of each equal-automorphism-cardinality fiber on exact complexity shells past a threshold index. Parity arguments cite it to move classes inside a fixed Aut-bucket without leaving the bucket. The body is a subtype equivalence: transport the shift, then restore the cardinality predicate via class-measure invariance.
Claim. Fix a tick map $\tau$ sending each exact path class of complexity $n$ to an element of $\mathrm{Fin}\,8$, and a tail antipodal shift $h$ for $\tau$. For every $n\ge N(h)$ and every $a\in\mathbb{N}$, the shift of $h$ restricts to a type equivalence $\{c\in\mathrm{ExactPathClass}_n:\lvert\mathrm{Aut}(c)\rvert=a\}\simeq\{c\in\mathrm{ExactPathClass}_n:\lvert\mathrm{Aut}(c)\rvert=a\}$.
background
This module banks the Aut-fiber parity-blocker surface for the Gap2 antipodal route. An exact path class is a combinatorially distinct exact complex of fixed complexity $n$ (exact shell, no cap type). Each class carries a positive per-class measure $\mathrm{classMu}$, defined as the reciprocal of the shell automorphism cardinality $\mathrm{shellAutCard},c=\lvert\mathrm{ExactAut}(\mathrm{out},c)\rvert$.
The equal-automorphism fiber $\mathrm{AutFiberBucket},n,a$ is the subtype of exact path classes of complexity $n$ with $\mathrm{shellAutCard},c=a$. A tail antipodal shift supplies, past a threshold $N$, a bijection on each exact shell that advances the Fin-8 tick by four (low/high hemispheres) and preserves $\mathrm{classMu}$. Because $\mathrm{classMu}=1/\mathrm{shellAutCard}$, mu-preservation is equivalent to automorphism-cardinality preservation, so the shift should close on each Aut-bucket.
The local design goal is the implication "inhabited tail antipodal shift $\Rightarrow$ eventual even Aut-bucket cardinalities," the combinatorial gate for a free antipodal matching inside each bucket.
proof idea
Build the equivalence by Equiv.subtypeEquiv on the underlying shell bijection h.shift n hn. The only obligation is that the subtype predicate $\mathrm{shellAutCard},c=a$ is invariant under the shift.
Both directions use the same bridge: h.mu_shift gives $\mathrm{classMu}(\mathrm{shift},c)=\mathrm{classMu},c$, and the sibling lemma equating equal class measures with equal shell automorphism cardinalities rewrites that equality into $\mathrm{shellAutCard}(\mathrm{shift},c)=\mathrm{shellAutCard},c$. Forward uses the equality transitively; reverse uses its symmetric form. No new combinatorial content is proved here.
why it matters
This private helper is the bucket-level transport step inside tailAutFiberEven_of_tailAntipodalShift, the abstract implication that an inhabited tail antipodal shift forces eventual even Aut-fiber bucket cardinalities. That implication is the positive half of the Gap2 R4 session 4B parity-blocker API: even buckets are the combinatorial gate for a free antipodal matching via the mu-preserving $+4$ tick shift on Fin-8 hemispheres.
In the broader SevenGaps gravity program, the dual terminal is the infinite-family odd-bucket obstruction (TailAutFiberParityBlocker), which would rule out any inhabited tail antipodal shift. The infinite blocker remains open; this definition only equips the positive direction. It does not flip the continuum-and-measure gap certificate and sits strictly inside the antipodal design path (eight-tick octave structure on exact shells).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.