lowEquivHigh
plain-language theorem explainer
Given a permutation that advances an 8-valued tick label by four steps, the low hemisphere (ticks 0–3) is bijective with the high hemisphere (ticks 4–7). Anyone proving even Aut-fiber cardinality under an antipodal tick shift cites this. The maps are the permutation and its inverse, with modular +4 lemmas swapping the two Fin-8 halves.
Claim. For any type $\alpha$, equivalence $e:\alpha\simeq\alpha$, and tick map $\tau:\alpha\to\mathrm{Fin}\,8$ with $\tau(e(a))=\tau(a)+4$ for all $a$, there is a type equivalence $\{a:\alpha\mid \tau(a).\mathrm{val}<4\}\simeq\{a:\alpha\mid 4\le\tau(a).\mathrm{val}\}$.
background
In the Gap2 R4 antipodal design, Aut-fiber buckets are equal-shellAutCard classes inside one exact shell. Even bucket cardinality is the combinatorial gate for a free antipodal matching; an infinite family of odd buckets is the credit-bearing obstruction (TailAutFiberParityBlocker, still open).
The eight-tick octave supplies $\mathrm{Fin},8$ labels. Low ticks are those with value in ${0,1,2,3}$; high ticks those in ${4,5,6,7}$. The lemmas val_add_four_low and val_add_four_high record that addition of 4 mod 8 swaps the hemispheres: low becomes high, high becomes low.
Module status: finite parity probes are measured externally (Bool only); the infinite blocker is defined but not proved; nothing here flips gap2_continuum_and_measure.
proof idea
Forward map: send a low-tick subtype witness $a$ to $e(a)$. Equivariance plus val_add_four_low puts $e(a)$ in the high hemisphere.
Inverse: send high $b$ to $e^{-1}(b)$. Rewrite equivariance at $e^{-1}(b)$. If $e^{-1}(b)$ were high, val_add_four_high would force $(\tau(e^{-1}b)+4).\mathrm{val}<4$, contradicting that $b$ is high after transport. Hence the preimage is low.
Left/right inverses are the standard symm_apply_apply / apply_symm_apply, lifted by Subtype.ext.
why it matters
This equivalence is the hemisphere-swap engine for even_card_of_tick_add_four: any finite type with a $+4$ tick-equivariant permutation has even cardinality, because low and high halves are equicardinal. That theorem is the local half of the abstract implication TailAntipodalShift $\Rightarrow$ TailAutFiberEven (mu-preserving $+4$ shift bijects hemispheres inside each Aut-bucket).
In the Recognition chain this sits on T7 (eight-tick octave, period $2^3$). Downstream it supports the antipodal route design surface for Gap2; the infinite parity blocker remains open, and this definition only supplies the tool used when a TailAntipodalShift is assumed. It does not close the continuum/measure gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.