Research proof index

σ_{-1}(X^e) = -X^{d-e} for 0 < e < d: the conjugate of a sub-d/2 monomial is minus the complementary monomial. The only nonzero coefficient of σ_{-1}(X^e) sits at d - e, with sign -1: from e·conjExp ≡ 2^{α+1} - e (mod 2^{α+1}) we get σ_{-1}(X^e) = X^{d + (d-e)} = -X^{d-e}.

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.