def Hex.DensePoly.cyclicCoeffs {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (p : DensePoly R) : Array R

Fold every coefficient into its exponent class modulo n, using one preallocated n-slot accumulator.

Equations

• Hex.DensePoly.cyclicCoeffs n p = List.foldl (Hex.DensePoly.addCyclicCoeff✝ n p) (Array.replicate n 0) (List.range p.size)

def Hex.DensePoly.negacyclicCoeffs {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (p : DensePoly R) : Array R

Fold every coefficient modulo x^n + 1, alternating the sign after each block of n exponents.

Equations

• Hex.DensePoly.negacyclicCoeffs n p = List.foldl (Hex.DensePoly.addNegacyclicCoeff✝ n p) (Array.replicate n 0) (List.range p.size)

def Hex.DensePoly.cyclicCoeff {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n k : Nat) (p : DensePoly R) : R

Sum coefficients of p whose exponents are congruent to k modulo n.

Equations

• Hex.DensePoly.cyclicCoeff n k p = (Hex.DensePoly.cyclicCoeffs n p).getD k 0

def Hex.DensePoly.negacyclicCoeff {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n k : Nat) (p : DensePoly R) : R

Alternating sum of coefficients in one congruence class, implementing reduction by x^n = -1.

Equations

• Hex.DensePoly.negacyclicCoeff n k p = (Hex.DensePoly.negacyclicCoeffs n p).getD k 0

theorem Hex.DensePoly.size_cyclicCoeffs {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (p : DensePoly R) : (cyclicCoeffs n p).size = n

The cyclic coefficient array has exactly the requested length.

theorem Hex.DensePoly.size_negacyclicCoeffs {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (p : DensePoly R) : (negacyclicCoeffs n p).size = n

The negacyclic coefficient array has exactly the requested length.

def Hex.DensePoly.mulCyclic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (_hn : 0 < n) (a b : DensePoly R) : DensePoly R

Cyclic convolution of positive length n.

Equations

• Hex.DensePoly.mulCyclic plan n _hn a b = Hex.DensePoly.ofCoeffs (Hex.DensePoly.cyclicCoeffs n (Hex.DensePoly.mulWith plan a b))

def Hex.DensePoly.mulNegacyclic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (_hn : 0 < n) (a b : DensePoly R) : DensePoly R

Negacyclic convolution of positive length n.

Equations

• Hex.DensePoly.mulNegacyclic plan n _hn a b = Hex.DensePoly.ofCoeffs (Hex.DensePoly.negacyclicCoeffs n (Hex.DensePoly.mulWith plan a b))

def Hex.DensePoly.mulCyclic? {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (a b : DensePoly R) : Option (DensePoly R)

Checked cyclic convolution; length zero has no quotient-ring meaning.

Equations

• Hex.DensePoly.mulCyclic? plan n a b = if hn : 0 < n then some (Hex.DensePoly.mulCyclic plan n hn a b) else none

def Hex.DensePoly.mulNegacyclic? {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (a b : DensePoly R) : Option (DensePoly R)

Checked negacyclic convolution; length zero has no quotient-ring meaning.

Equations

• Hex.DensePoly.mulNegacyclic? plan n a b = if hn : 0 < n then some (Hex.DensePoly.mulNegacyclic plan n hn a b) else none

theorem Hex.DensePoly.size_mulCyclic_le {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (hn : 0 < n) (a b : DensePoly R) : (mulCyclic plan n hn a b).size ≤ n

Cyclic products contain at most n stored coefficients.

theorem Hex.DensePoly.size_mulNegacyclic_le {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (hn : 0 < n) (a b : DensePoly R) : (mulNegacyclic plan n hn a b).size ≤ n

Negacyclic products contain at most n stored coefficients.

theorem Hex.DensePoly.coeff_mulCyclic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (hn : 0 < n) (a b : DensePoly R) (i : Nat) : (mulCyclic plan n hn a b).coeff i = if i < n then cyclicCoeff n i (a * b) else 0

Coefficient description of cyclic folding.

theorem Hex.DensePoly.coeff_mulNegacyclic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (hn : 0 < n) (a b : DensePoly R) (i : Nat) : (mulNegacyclic plan n hn a b).coeff i = if i < n then negacyclicCoeff n i (a * b) else 0

Coefficient description of negacyclic folding.

theorem Hex.DensePoly.ofCoeffs_cyclicCoeffs {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (p : DensePoly R) : ofCoeffs (cyclicCoeffs n p) = List.foldl (fun (q : DensePoly R) (i : Nat) => q + monomial (i % n) (p.coeff i)) 0 (List.range p.size)

Cyclic folding sums monomials with degrees reduced modulo the length.

def Hex.DensePoly.negacyclicResidue {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n i : Nat) (c : R) : DensePoly R

The signed residue of c * x^i modulo x^n + 1.

Equations

• Hex.DensePoly.negacyclicResidue n i c = if i / n % 2 = 0 then Hex.DensePoly.monomial (i % n) c else Hex.DensePoly.monomial (i % n) (0 - c)

def Hex.DensePoly.negacyclicTerm {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (p : DensePoly R) (i : Nat) : DensePoly R

The signed monomial contributed by coefficient i when reducing modulo x^n + 1.

Equations

• Hex.DensePoly.negacyclicTerm n p i = Hex.DensePoly.negacyclicResidue n i (p.coeff i)

theorem Hex.DensePoly.ofCoeffs_negacyclicCoeffs {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (p : DensePoly R) : ofCoeffs (negacyclicCoeffs n p) = List.foldl (fun (q : DensePoly R) (i : Nat) => q + negacyclicTerm n p i) 0 (List.range p.size)

Negacyclic folding sums degree-reduced monomials with alternating signs.