Cyclotomic Moduli over CPolynomial

This file defines the modulus data that turns a computable polynomial type CompPoly.CPolynomial R into the cyclotomic ring R[X] / (Φ_m).

Because Mathlib's Polynomial.cyclotomic is noncomputable (it routes through roots of unity in ℂ), we cannot build the modulus by evaluating cyclotomic. Instead a CyclotomicModulus bundles an explicit computable polynomial φ : CPolynomial R (e.g. X^d + 1) together with

• a proof that φ is monic (needed for CompPoly's modByMonic-based reduction),
• its conductor m, and
• a proof linking it to the genuine cyclotomic polynomial, φ.toPoly = Polynomial.cyclotomic m R.

The canonical Hachi [NOZ26] instantiation is the power-of-two cyclotomic φ = X^{2^α} + 1, of conductor 2^{α+1}, provided as powTwoCyclotomic.

To keep the executable layer free of any noncomputable contamination, the data and the proofs are kept in separate structures:

• CyclotomicModulus R is pure computable data (φ, conductor); reduction, multiplication and the vector/matrix operations depend only on it, so the canonical Hachi instance is fully #eval-able.
• IsCyclotomic Φ is a Prop-class bundling the two proof obligations (monic, isCyclotomic); only the (noncomputable) semantic bridge needs it.

Main definitions

• CyclotomicModulus R — the computable modulus data.
• IsCyclotomic Φ — the cyclotomic-correctness proofs for a modulus.
• CyclotomicModulus.powTwoCyclotomic α — the Hachi modulus X^{2^α} + 1 (computable), with its IsCyclotomic instance.

References

• [Nguyen, N. K., O'Rourke, G., and Zhang, J., Hachi: Efficient Lattice-Based Multilinear Polynomial Commitments over Extension Fields][NOZ26]

@[simp]

theorem CompPoly.CPolynomial.toPoly_X {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] : X.toPoly = Polynomial.X

CPolynomial.X.toPoly = Polynomial.X.

structure ArkLib.Lattices.CyclotomicModulus (R : Type u_1) [Field R] [BEq R] [LawfulBEq R] : Type u_1

Computable data describing a cyclotomic modulus for the polynomial ring over R: an explicit, computable polynomial φ : CPolynomial R (e.g. X^d + 1) together with its conductor m. This structure carries no proofs, so the reduction and ring operations built on it (reduce, mul, matVecMul, …) stay fully computable. The cyclotomic-correctness proofs live separately in IsCyclotomic.

• φ : CompPoly.CPolynomial R

  The explicit computable modulus polynomial, e.g. X^d + 1.

• conductor : ℕ

  The conductor m: φ is the m-th cyclotomic polynomial.

class ArkLib.Lattices.IsCyclotomic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (Φ : CyclotomicModulus R) : Prop

Cyclotomic-correctness proofs for a modulus Φ: that φ is monic (so CompPoly's modByMonic reduction applies) and that, as a Mathlib polynomial, φ is the conductor-th cyclotomic polynomial (so the reduced ring really is R[X] / (Φ_m)). A Prop-class, supplied by instance resolution to the semantic bridge without touching the executable layer.

• monic : Φ.φ.toPoly.Monic

  φ is monic.

• isCyclotomic : Φ.φ.toPoly = Polynomial.cyclotomic Φ.conductor R

  φ is, as a Mathlib polynomial, the conductor-th cyclotomic polynomial.

def ArkLib.Lattices.CyclotomicModulus.powTwoCyclotomic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (α : ℕ) : CyclotomicModulus R

The power-of-two cyclotomic modulus φ = X^{2^α} + 1, the cyclotomic polynomial of conductor 2^{α+1}. This is the ring of integers of the 2^{α+1}-th cyclotomic field, used as R_q := Z_q[X] / (X^d + 1) with d = 2^α throughout lattice-based proof systems. Computable: the operations built on it can be #eval-ed.

instance ArkLib.Lattices.CyclotomicModulus.powTwoCyclotomic_isCyclotomic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (α : ℕ) : IsCyclotomic (powTwoCyclotomic α)

The modulus X^{2^α} + 1 is the 2^{α+1}-th cyclotomic polynomial.