Research proof index

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

σ_i fixes 1, since only the constant term contributes (so in particular σ_1 fixes it).

Multiplicativity of the computable automorphism, transported from galoisAutₛ (a RingHom) through the soundness bridge.

(S5) The core polynomial identity behind soundness: the monomial-remapped sum (before reduction) equals aeval (X^i) of the underlying polynomial. Both sides are ∑_{k<d} X^{ki}·a_k.

σ_m (X^i) = X^{i·m} (reduced). For i < 2^α the monomial-remap defining galoisAut collapses to the single surviving term. This is the key input to the trace-of-monomial computation in TraceInnerProduct.lean.

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.