Research proof index

The conjugate σ_{-1}(X^e) lands at position d - e (mod d), for 0 < e < d.

(Phase 1) −1 ∉ ⟨q⟩ in (Z/2^{α+1})ˣ, stated as: no power of q equals −1. For q ≡ 5 (mod 8), every power of q is ≡ 1 (mod 4) (since q ≡ 1 (mod 4)), while −1 ≡ 3 (mod 4) (as α ≥ 1, so 4 ∣ 2^{α+1}); projecting to ZMod 4 separates them. This is the precise sense in which q ≡ 5 (mod 8) forces σ_{-1} to swap the two CRT factors.

The multiplicative order of q modulo 2^(α+1) is 2^(α-1), phrased to match ZMod.irreducible_of_dvd_cyclotomic_of_natDegree (K = ZMod q, n = 2^(α+1)).

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...

Well-definedness on the power-of-two ring: aeval (X^i) maps the modulus ideal into itself for odd i, since X^{2^α} + 1 ∣ (X^{2^α})^i + 1.