Research proof index

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.

|H| = d/k = 2^α / k (Hachi [NOZ26, §3], from |⟨4k+1⟩| = d/(2k) and the ± factor). The hypotheses match Hachi [NOZ26, §3, Claim 1] / [LS18, Lem 2.4]: k is a power of two (hk2pow) and divides d/2, i.e. 2k ∣ d = 2^α (hk). Both are needed for 4k+1 to have order exactly d/(2k) in (Z/2^{α+1})ˣ; the weaker k ∣ 2^α (= k ∣ d) does not suf...

Multiplication by a generator permutes Hexp (as a Finset), i.e. the image under i ↦ (g·i) mod 2^{α+1} is Hexp itself, for g a generator of H = ⟨σ_{-1}, σ_{4k+1}⟩. This is the group-translation fact g • H = H transported through the Hexp ↔ H bridge. Proof: the number-theoretic input (two_pow_dvd_four_pow_sub_one_iff ⟹ `(4k+1)^{2^{α-κ-1}}...

Every exponent enumerated by Hexp is odd (so the corresponding σ_i is a genuine automorphism). The base 4k+1 is odd; reduction mod the even conductor 2^{α+1} and the (m − ·) reflection both preserve oddness.