Research proof index

(Phase 2) Φ_{2^{α+1}} over Z_q has exactly two distinct monic irreducible factors, each of degree 2^{α-1} = d/2, for q ≡ 5 (mod 8). From Mathlib's normalizedFactors_cyclotomic_card (count = φ(2^{α+1}) / ord = 2^α / 2^{α-1} = 2) and natDegree_of_mem_normalizedFactors_cyclotomic (degree = ord = 2^{α-1}), using orderOf_q_eq.

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