Research proof index

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.

Every σ_m with m ∈ Hexp fixes R_q^H: modulo 2d, m is ±(4k+1)^a, and the two generators σ_{4k+1}, σ_{-1} fix R_q^H (so does any composite).