splitLowHigh
plain-language theorem explainer
Canonical equivalence that partitions any type labeled by Fin 8 into the low hemisphere (tick value < 4) and the high hemisphere (tick value ≥ 4). Downstream parity arguments cite it to turn a +4 tick-equivariant bijection into equal cardinalities of the two halves. The construction is a pure case split on the tick value, with inverse forgetting the subtype proof.
Claim. Let $\alpha$ be any type and $\tau:\alpha\to\mathrm{Fin}\,8$ a tick labeling. Write $L=\{a\in\alpha:\tau(a)<4\}$ and $H=\{a\in\alpha:\tau(a)\ge 4\}$. Then there is a canonical equivalence $\alpha\simeq L\oplus H$ sending each point to its low or high summand according as its tick value is less than $4$ or not.
background
The ambient module banks the Aut-fiber parity-blocker surface for the Gap2 antipodal route. The eight-tick octave (period $2^3$) is the fundamental RS evolution period; a map $\tau:\alpha\to\mathrm{Fin},8$ assigns each point a phase in that octave.
TickLow and TickHigh are the two hemispheres: subtype of points with tick value strictly below $4$, and subtype with value at least $4$. A free antipodal matching on an Aut-bucket is expected to act as a $+4$ tick shift, swapping these hemispheres inside each equal-shellAutCard class.
The design implication is that a $\mu$-preserving $+4$ tick shift bijects low and high halves, so each Aut-bucket that admits such a shift must have even cardinality (TailAutFiberEven). An infinite family of odd buckets would obstruct any inhabited antipodal shift (TailAutFiberParityBlocker).
proof idea
Definitional construction of an equivalence, not a deep lemma. Forward map: case on whether $(\tau a).\mathrm{val}<4$; send $a$ to the left summand with that proof, or to the right summand via Nat.le_of_not_lt. Inverse forgets the subtype witness on either summand. Left inverse: by_cases on the same predicate and simp. Right inverse: on the left summand simp with the stored inequality; on the right, rewrite $\neg(\mathrm{val}<4)$ from $\mathrm{val}\ge 4$ and simp.
why it matters
Local plumbing for the hemisphere-split argument that turns a $+4$ tick-equivariant permutation into even cardinality. The sole downstream consumer is even_card_of_tick_add_four, whose doc-comment states: a $+4$ tick-equivariant permutation of a finite type has even cardinality because the low/high Fin-8 hemispheres are equicardinal. That theorem opens with Fintype.card_congr (splitLowHigh tau).
In the Gap2 R4 antipodal design, this is the combinatorial gate from TailAntipodalShift to TailAutFiberEven: equal halves force even Aut-bucket size. The infinite odd-bucket obstruction remains OPEN; the finite parity probe is only MEASURED externally. The eight-tick octave (T7) is the structural reason the split is at $4$ rather than an arbitrary cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.