Documentation

ArkLib.Data.Lattices.CyclotomicRing.NormBounds.LyubashevskySeiler

Lyubashevsky–Seiler: Short Elements Are Invertible #

The Lyubashevsky–Seiler invertibility result [LS18, Corollary 1.2]; recalled as Lemma 3 of the Hachi paper [NOZ26]: over the power-of-two cyclotomic modulus φ = X^{2^α} + 1 (powTwoCyclotomic α) with a prime q ≡ 5 (mod 8), a nonzero element of Rq (powTwoCyclotomic α) = ZMod q[X]/(X^{2^α}+1) whose centered Euclidean norm is below √q is a unit.

The statement is deliberately pinned to powTwoCyclotomic α (X^{2^α}+1): LS18 Cor. 1.2 is the k = 2 splitting case (q ≡ 2·2+1 ≡ 5 (mod 8), Euclidean bound q^{1/2} = √q), and that splitting / minimum-distance analysis is specific to the negacyclic ring. For a general cyclotomic Φ_m of power-of-two degree (e.g. Φ₁₅, Φ₁₂) the q ≡ 5 (mod 8) condition and the √q bound are simply wrong, so phrasing the lemma for an arbitrary Φ with deg φ = 2^α would be unsound.

This is one of the two unproven lemmas for the Greyhound [NS24] / Hachi [NOZ26] weak-binding argument; the other is scalarVecMul_mul_l2NormSq_le in NormBounds.MicciancioYoung.

Overview #

Write n := 2^α. The argument is the k = 2 splitting case and reduces to an elementary mod q divisibility count, needing no ideal lattices, canonical embedding, or Minkowski bound.

Since q ≡ 5 (mod 8), -1 is a square in ZMod q (ZMod.exists_sq_eq_neg_one_iff), say r^2 = -1, and the negacyclic modulus splits as X^n + 1 = (X^{n/2} - r)(X^{n/2} + r). Both factors are irreducible over ZMod q: the multiplicative order of q modulo 2^{α+1} is 2^{α-1} (lifting-the-exponent, v₂(q^{2^k} - 1) = k + 2), so every irreducible factor of cyclotomic (2^{α+1}) (ZMod q) = X^n + 1 has degree n/2, which forces each degree-n/2 factor to be irreducible.

A non-unit c is therefore not coprime to X^n + 1, so one factor g = X^{n/2} - s (s = ±r, s^2 = -1) divides its lift ; evaluating at a root ζ of g (so ζ^{n/2} = s) gives c̃(ζ) = Σ_{j<n/2} (c̃_j + s·c̃_{n/2+j}) ζ^j = 0. As 1, …, ζ^{n/2-1} are independent over ZMod q, each c̃_j + s·c̃_{n/2+j} = 0, and squaring (s^2 = -1) gives q ∣ (c̃_j² + c̃_{n/2+j}²) over . Summing, q ∣ ‖c‖₂². With ‖c‖₂² ≤ ‖c‖₁² ≤ κ² < q this forces ‖c‖₂² = 0, hence c = 0, contradicting ‖c‖₁ > 0. (Edge case α = 0: Rq is a field, so a nonzero element is a unit.)

The supporting lemmas live in NormBounds.LsCore (the iso Rq.equivQuotient, the order computation orderOf_q_mod_two_pow, the irreducibility irreducible_X_pow_sub_C_r, and the coefficient kernel dvd_sq_add_sq); the splitting and √-1 existence are powTwoCyclotomic_splits_of_sq_eq_neg_one and exists_sq_eq_neg_one_of_mod_eight_eq_five.

References #

Norm bridge. The centered squared ℓ₂ norm is at most the square of the centered ℓ₁ norm: ‖c‖₂² ≤ ‖c‖₁². This is Σ aₖ² ≤ (Σ aₖ)² for nonnegative aₖ.

For a prime q ≡ 5 (mod 8) we have q % 4 = 1 ≠ 3, so -1 is a square in ZMod q (ZMod.exists_sq_eq_neg_one_iff). This r (r² = -1) drives the explicit splitting.

theorem ArkLib.Lattices.CyclotomicModulus.powTwoCyclotomic_splits_of_sq_eq_neg_one {q : } [Fact (Nat.Prime q)] (α : ) {r : ZMod q} (hr : r ^ 2 = -1) ( : 1 α) :
(Polynomial.X ^ 2 ^ (α - 1) - Polynomial.C r) * (Polynomial.X ^ 2 ^ (α - 1) + Polynomial.C r) = Polynomial.X ^ 2 ^ α + 1

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.

(powTwoCyclotomic α).φ.toPoly = X^(2^α) + 1.

(powTwoCyclotomic α).φ.natDegree = 2^α.

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

theorem ArkLib.Lattices.CyclotomicModulus.q_dvd_l2NormSq_of_not_isUnit {q : } [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZMod q)] (α : ) (hq5 : q % 8 = 5) {c : (powTwoCyclotomic α).Rq} (hc : ¬IsUnit c) :

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; evaluating at the root ζ of AdjoinRoot φᵢ (ζ^{2^{α-1}} = ±r, s² = -1) and using the degree-2^{α-1} independence of 1,…,ζ^{2^{α-1}-1} (dvd_sq_add_sq) gives q ∣ (c̃_j² + c̃_{2^{α-1}+j}²) per j; summing yields q ∣ ‖c‖₂². Edge case α = 0: Rq Φ is a field, so a non-unit is 0.

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.

theorem ArkLib.Lattices.CyclotomicModulus.isUnit_of_l1Norm_le {q : } [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZMod q)] (α : ) (hq5 : q % 8 = 5) {c : (powTwoCyclotomic α).Rq} {κ : } (hpos : 0 < Rq.l1Norm (powTwoCyclotomic α) c) (hle : Rq.l1Norm (powTwoCyclotomic α) c κ) ( : κ ^ 2 < q) :

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‖₂², while ‖c‖₂² ≤ ‖c‖₁² ≤ κ² < q, so ‖c‖₂² = 0, forcing c = 0 against ‖c‖₁ > 0.