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

Factor existence. For q ≡ 5 (mod 8), X^{2^α}+1 factors over Z_q as a product of two coprime irreducible polynomials. Extracted from cyclotomic_card_normalizedFactors (the two normalized factors), with coprimality from Irreducible.coprime_iff_not_dvd.

R_q^H is a field (Hachi [NOZ26, §3, Lemma 5], field part). Since R_q^H ⊆ R_q^{σ_{-1}} (fixedSubring_le_conjFixedSubring) and the latter is a field (conjFixedSubring_isField), R_q^H is a finite integral domain, hence a field. Proven modulo conjFixedSubring_isField: the inclusion R_q^H ↪ R_q^{σ_{-1}} is an injective ring hom into a field,...

Hachi [NOZ26, §3, Lemma 5]: R_q^H ≅ F_{q^k}. For q ≡ 5 (mod 8) and 2·2^κ ∣ 2^α, the fixed subring is ring-isomorphic to GaloisField q (2^κ) (= F_{q^{2^κ}}). Combines fixedSubring_isField with card_fixedSubring_eq (|R_q^H| = q^{2^κ}) and the classification of finite fields by cardinality. Proven modulo conjFixedSubring_isField (via `f...

Core unit lemma. In S = Z_q[X]/(X^{2^α}+1), every nonzero σ_{-1}-fixed element is a unit. If b = mk g is not a unit then g shares a factor p_i with X^{2^α}+1 = p₁p₂; the reverse identity plus the swap p₁.reverse ~ p₂ force g to be divisible by both p₁ and p₂, hence by X^{2^α}+1, so b = 0.

The reverse identity. In S = Z_q[X]/(X^{2^α}+1), the conjugation σ_{-1} (here the semantic automorphism galoisAutₛ of exponent conjExp = 2^{α+1}-1) and the polynomial reversal are related by mk(reverse p) = σ_{-1}(mk p) · (mk X)^{deg p}. This is the concrete handle behind "σ_{-1} swaps the two factors": since (mk X)^{deg p} is a unit, `σ...