11.3. Principal operations🔗

The headline operations all work in the quotient ring `Fₚ[x] / (f)` for a monic modulus f. Modular exponentiation raises a base to a power and reduces, and modular composition substitutes one polynomial into another and reduces. Both use Horner-style loops that re-reduce at every step, so intermediate results never grow past the modulus degree.

def

Hex.FpPoly.powModMonic {p : Nat} [Hex.ZMod64.Bounds p]
  (base f : Hex.FpPoly p) (hmonic : Hex.DensePoly.Monic f) (n : Nat) :
  Hex.FpPoly p
Hex.FpPoly.powModMonic {p : Nat}
  [Hex.ZMod64.Bounds p]
  (base f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f)
  (n : Nat) : Hex.FpPoly p

Compute base^n mod f for monic f.

def

Hex.FpPoly.composeModMonic {p : Nat} [Hex.ZMod64.Bounds p]
  (f g modulus : Hex.FpPoly p) (hmonic : Hex.DensePoly.Monic modulus) :
  Hex.FpPoly p
Hex.FpPoly.composeModMonic {p : Nat}
  [Hex.ZMod64.Bounds p]
  (f g modulus : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic modulus) :
  Hex.FpPoly p

Horner-style modular composition in the quotient F_p[x] / (modulus).

The reduction after each multiplication keeps the intermediate polynomials bounded by the modulus degree while preserving the same result as composing first and reducing once at the end.

The finite-field irreducibility and factorization tests are built on the Frobenius-power maps. Hex.FpPoly.frobeniusXMod computes X^p mod f, and Hex.FpPoly.frobeniusXPowMod iterates it to X^(pᵏ) mod f for arbitrary k.

def

Hex.FpPoly.frobeniusXMod {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (hmonic : Hex.DensePoly.Monic f) : Hex.FpPoly p
Hex.FpPoly.frobeniusXMod {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f) :
  Hex.FpPoly p

Compute X^p mod f, the basic Frobenius generator used downstream.

def

Hex.FpPoly.frobeniusXPowMod {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (hmonic : Hex.DensePoly.Monic f) (k : Nat) :
  Hex.FpPoly p
Hex.FpPoly.frobeniusXPowMod {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f)
  (k : Nat) : Hex.FpPoly p

Compute X^(p^k) mod f for arbitrary k.

Square-free decomposition runs Yun's algorithm over `Fₚ`. The result bundles a scalar unit with a list of square-free factors and their multiplicities. The two record types name those pieces.

structure

Hex.FpPoly.SquareFreeFactor (p : Nat) [Hex.ZMod64.Bounds p] : Type
Hex.FpPoly.SquareFreeFactor (p : Nat)
  [Hex.ZMod64.Bounds p] : Type

One square-free factor together with its multiplicity.

Constructor

Hex.FpPoly.SquareFreeFactor.mk

Fields

factor : Hex.FpPoly p

The square-free factor polynomial.

multiplicity : Nat

The exponent with which factor divides the original polynomial.

structure

Hex.FpPoly.SquareFreeDecomposition (p : Nat) [Hex.ZMod64.Bounds p] :
  Type
Hex.FpPoly.SquareFreeDecomposition
  (p : Nat) [Hex.ZMod64.Bounds p] : Type

A square-free decomposition records the scalar unit and the nonconstant factors.

Constructor

Hex.FpPoly.SquareFreeDecomposition.mk

Fields

unit : Hex.ZMod64 p

The leading-coefficient scalar unit pulled out of the polynomial.

factors : List (Hex.FpPoly.SquareFreeFactor p)

The square-free factors together with their multiplicities.

def

Hex.FpPoly.squareFreeDecomposition {p : Nat} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p) (f : Hex.FpPoly p) :
  Hex.FpPoly.SquareFreeDecomposition p
Hex.FpPoly.squareFreeDecomposition
  {p : Nat} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p)
  (f : Hex.FpPoly p) :
  Hex.FpPoly.SquareFreeDecomposition p

Compute a square-free decomposition by normalizing away the leading scalar and running Yun's algorithm on the resulting monic polynomial.

The inverse operation reassembles a polynomial from a decomposition by raising each factor to its multiplicity and multiplying. It is the reconstruction side of the correctness laws below.

def

Hex.FpPoly.weightedProduct {p : Nat} [Hex.ZMod64.Bounds p]
  (factors : List (Hex.FpPoly.SquareFreeFactor p)) : Hex.FpPoly p
Hex.FpPoly.weightedProduct {p : Nat}
  [Hex.ZMod64.Bounds p]
  (factors :
    List
      (Hex.FpPoly.SquareFreeFactor p)) :
  Hex.FpPoly p

Multiply the factors in a square-free decomposition with their multiplicities.