Research proof index

R_q^{σ_{-1}} is a field (blueprint Theorem, Phase 5). For q ≡ 5 (mod 8), every nonzero σ_{-1}-fixed element is a unit: if p₁ ∣ g then the reverse identity plus the swap p₁.reverse ~ p₂ force p₂ ∣ g too, so X^{2^α}+1 ∣ g and the element vanishes. Proven (modulo no_selfReciprocal_factor): transport to S = Z_q[X]/(X^{2^α}+1) via `Rq.equ...

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

X^(2^(α-1)) - C r divides X^(2^α)+1 when r^2 = -1 and α ≥ 1.

2-adic LTE for g = 4·2^κ + 1: v₂(gⁿ − 1) = (κ+2) + v₂(n).

The 2-adic valuation of q^(2^k) - 1 is k + 2.

For a prime q with q % 8 = 5, q - 1 ≡ 4 (mod 8), hence v₂(q-1) = 2.