Research proof index

Splitting into explicit factors. Over ZMod q, given r² = -1, the negacyclic modulus X^{2^α}+1 factors as (X^{2^{α-1}} - r)·(X^{2^{α-1}} + r) for α ≥ 1. These are the two degree-2^{α-1} pieces of the LS k = 2 splitting; over q ≡ 5 (mod 8) they are irreducible (the order-of-q argument), which is what makes the CRT factors fields.

ψ is bijective (Hachi [NOZ26, §3, Theorem 2]): injective (from the non-degenerate trace pairing, psi_injective) and a cardinality match |(R_q^H)^{d/k}| = (q^k)^{d/k} = q^d = |R_q|.

ψ is injective (Hachi [NOZ26, §3, Theorem 2]). The trace form (a,b) ↦ ⟨a,b⟩ is non-degenerate (testing against b = eⱼ recovers aⱼ), and d/k is a unit in R_q (it is a power of 2, invertible since q is odd). So ψ(a) = ψ(b) forces ⟨a,eⱼ⟩ = ⟨b,eⱼ⟩, i.e. aⱼ = bⱼ, for every j.

Vanishing outside the matching residue classes. If j's index does not match p's residue class mod d/2k, the p-th coefficient of the j-th packed summand a_j · X^{packExp j} is 0. Combined with packExp_mod_eq and the support of fixed elements (fixedSubring_coeff_eq_zero), only summands whose index agrees with p mod d/2k can contrib...

Algebraic core. If c : Rq Φ over q ≡ 5 (mod 8) is not a unit, then q divides its centered squared ℓ₂ norm. A non-unit's image in (ZMod q)[X]/(X^{2^α}+1) is non-coprime to the modulus, so an irreducible factor φᵢ = X^{2^{α-1}} ∓ r of X^{2^α}+1 (powTwoCyclotomic_splits_of_sq_eq_neg_one, irreducible_X_pow_sub_C_r) divides its lift; ev...

Reduction modulo φ is invisible in the quotient: reduce p ≡ p (mod φ). This is the cyclotomic analogue of the NegacyclicRingSemantics soundness data.