Univariate Algorithm Contexts

Algorithm dictionaries for reusable univariate polynomial operations, including canonical, NTT, and NTTFast-backed implementations.

structure CompPoly.CPolynomial.MulContext (R : Type u_2) [Semiring R] [BEq R] [LawfulBEq R] : Type u_2

Explicit multiplication backend for univariate polynomial algorithms.

• mul : CPolynomial R → CPolynomial R → CPolynomial R

  Multiply two canonical polynomials.

• mul_eq_mul (p q : CPolynomial R) : self.mul p q = p * q

  The backend agrees with canonical polynomial multiplication.

structure CompPoly.CPolynomial.ModContext (R : Type u_2) [Field R] [BEq R] [LawfulBEq R] : Type u_2

Explicit remainder backend for algorithms that only need reduction modulo monic divisors.

• modByMonic : CPolynomial R → CPolynomial R → CPolynomial R

  Reduce the first polynomial modulo the second, assuming the divisor is monic.

• modByMonic_eq_modByMonic (p q : CPolynomial R) : self.modByMonic p q = p.modByMonic q

  The backend agrees with the canonical monic-remainder operation.

def CompPoly.CPolynomial.MulContext.naive {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : MulContext R

The default multiplication context, backed by canonical CPolynomial multiplication.

def CompPoly.CPolynomial.MulContext.ntt {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) : MulContext R

NTT-backed multiplication context with canonical multiplication for unsupported lengths.

The context asks the selector for a domain that fits the current operands. If no supported domain is available, it uses ordinary CPolynomial multiplication.

def CompPoly.CPolynomial.MulContext.nttFast {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) : MulContext R

NTTFast-backed multiplication context with canonical multiplication for unsupported lengths.

The context asks the selector for a domain that fits the current operands. If no supported domain is available, it uses ordinary CPolynomial multiplication.

def CompPoly.CPolynomial.ModContext.naive {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] : ModContext R

The default monic-remainder context, backed by CPolynomial.modByMonic.

def CompPoly.CPolynomial.ModContext.remainderOnly {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] : ModContext R

A remainder-only backend for monic remainders.

def CompPoly.CPolynomial.ModContext.reversal {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : Raw.MulLowContext R) : ModContext R

A reversal-based monic-remainder backend parameterized by low-product multiplication.

def CompPoly.CPolynomial.ModContext.reversalNtt {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) : ModContext R

Monic remainders by reversal, using an NTT low-product backend.

def CompPoly.CPolynomial.ModContext.reversalNttFast {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (NTT.FittingDomain R requiredLen)) : ModContext R

Monic remainders by reversal, using an NTTFast low-product backend.