Research proof index

At most two packed indices share a residue class mod d/2k. Given a residue r with j ≡ r (mod d/2k = 2^{α-κ-1}), the index j : Fin (d/2^κ) is either the first-half witness (value r) or the second-half witness (value d/2k + r). Combined with packExp_mod_eq, this pins down exactly which (at most two) packed summands can contribute to a give...

Packing exponents stay in range: for 2·2^κ ∣ 2^α, every packed exponent packExp α (2^κ) j lands below the ring dimension d = 2^α, for j ranging over the packed index set Fin (d/2^κ).

Alignment of the second half after the X^{d/2} shift: packExp α (2^κ) j is congruent to j modulo d/2k = 2^{α-κ-1}, on both halves of the index range. On the first half this is rfl (no shift); on the second half the shift 2^{α-1} = 2^κ·2^{α-κ-1} is a multiple of 2^{α-κ-1}, so it vanishes mod 2^{α-κ-1}. This is what lets a single output...