Research proof index

If a is coprime to f then Ideal.Quotient.mk (span {f}) a is a unit.

Lyubashevsky–Seiler: short elements are invertible (LS18, Cor. 1.2; Hachi, Lemma 3). Over the power-of-two cyclotomic modulus powTwoCyclotomic α (φ = X^{2^α}+1) with a prime q ≡ 5 (mod 8), a nonzero element of Rq (powTwoCyclotomic α) with centered ℓ₁ norm ≤ κ and κ² < q is a unit: by the algebraic core a non-unit forces q ∣ ‖c‖₂², whil...

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.

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

A ring element with zero centered squared ℓ₂ 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.