Research proof index

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

The geometric sum ∑_{j<d/2k} (X^{4ki})^j = 0 when d/2k ∤ i. The ratio r = X^{4ki} satisfies r^{d/2k} = X^{2di} = 1, and r - 1 is a unit (Xpow_sub_one_isUnit, since X^{4ki·2^t} = -1 for a suitable t extracted from the 2-adic valuation of i).

Claim 1 reindex: ∑_{a<n} X^{i·((4k+1)^a mod 2d)} = X^i·∑_{j<n} (X^{4ki})^j. The subgroup ⟨4k+1⟩ = {(4k+1)^a mod 2d} equals the arithmetic progression {4k·j+1 : j<n} (both have n distinct elements, and (4k+1)^a ≡ 1 mod 4k), which linearizes the exponent and exposes the geometric series.

The power gⁿ mod 2^{α+1} depends only on n mod 2^{α-κ-1} (period = order of g).

Composition law σ_i ∘ σ_j = σ_{ij} (for i, j odd, so the maps are genuine automorphisms). Proven on the semantic aeval side via the soundness bridge galoisAut_toQuotient and aeval_X_pow_aeval_X_pow.