Research proof index

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.

A reduced representative has zero coefficients at and beyond deg φ.

Multiplying by the constant constRq Φ c scales coefficients by c.

The constant constRq Φ c has underlying polynomial C c (no reduction occurs, as deg (C c) = 0 < deg φ).

A ring element with zero centered ℓ₁ norm is 0: every centered coefficient representative below deg φ vanishes (ZMod.valMinAbs_eq_zero), and the representative is reduced (degree < deg φ), so the underlying polynomial is 0.