hex

11.4. The quotient by a modulus🔗

HexPolyFp packages the quotient `Fₚ[x] / (g)` as a type of canonical representatives: each element stores the unique polynomial of degree below the modulus, together with a proof of that bound.

🔗structure
Hex.FpPoly.Quotient {p : Nat} [Hex.ZMod64.Bounds p] (g : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic g)
  (hg_pos : 0 < (Hex.DensePoly.degree? g).getD 0) : Type
Hex.FpPoly.Quotient {p : Nat}
  [Hex.ZMod64.Bounds p] (g : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic g)
  (hg_pos :
    0 <
      (Hex.DensePoly.degree? g).getD 0) :
  Type

Canonical representatives for the quotient F_p[X] / (g), reduced modulo a monic positive-degree modulus.

Constructor

Hex.FpPoly.Quotient.mk

Fields

val : Hex.FpPoly p

The chosen representative polynomial, of degree below g.

reduced : (Hex.DensePoly.degree? self.val).getD 0 < (Hex.DensePoly.degree? g).getD 0

The representative's degree is strictly below that of the modulus g.

The quotient is unconditionally a commutative ring. It becomes a field only when g is irreducible, and HexPolyFp parametrizes over that fact rather than deciding it. There is no unconditional Field instance. Instead the field-promoting laws are theorems that take FpPoly.Irreducible g as an explicit hypothesis. A downstream caller supplies an irreducibility witness (in practice a checkable Rabin certificate from HexBerlekamp), and only then are inverses available. The inverse-cancellation laws are stated in Key correctness theorems.

11.4.1. Worked example: arithmetic over F₅🔗

The block below works over FpPoly 5. It fixes the monic quadratic modulus x² + 2 (whose reduction rule is x² ≡ -2 ≡ 3 (mod 5)) and a linear modulus x + 3, then runs modular exponentiation, Frobenius, composition, weighted products, and square-free decomposition. The helper coeffNats converts a polynomial to a list of natural-number coefficients. The expected values are the same ones pinned by the library's conformance suite.

open Hex Hex.FpPoly namespace HexPolyFpChapterExample private instance : ZMod64.Bounds 5 := ⟨⊢ 0 < 5 All goals completed! 🐙, ⊢ 5 ≤ UInt64.word All goals completed! 🐙⟩ private theorem one_ne_zero_five : (1 : ZMod64 5) ≠ 0 := ⊢ 1 ≠ 0 h:1 = 0⊢ False h:1 = 0hm:1 % 5 = 0 % 5⊢ False All goals completed! 🐙 private theorem prime_five : Hex.Nat.Prime 5 := ⊢ Nat.Prime 5 ⊢ 2 ≤ 5⊢ ∀ (m : Nat), m ∣ 5 → m = 1 ∨ m = 5 ⊢ 2 ≤ 5 All goals completed! 🐙 ⊢ ∀ (m : Nat), m ∣ 5 → m = 1 ∨ m = 5 m:Nathm:m ∣ 5⊢ m = 1 ∨ m = 5 m:Nathm:m ∣ 5hmle:m ≤ 5⊢ m = 1 ∨ m = 5 m:Nathm:m ∣ 5hmle:m ≤ 5hcases:m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 ∨ m = 5⊢ m = 1 ∨ m = 5 hm:0 ∣ 5hmle:0 ≤ 5⊢ 0 = 1 ∨ 0 = 5hm:1 ∣ 5hmle:1 ≤ 5⊢ 1 = 1 ∨ 1 = 5hm:2 ∣ 5hmle:2 ≤ 5⊢ 2 = 1 ∨ 2 = 5hm:3 ∣ 5hmle:3 ≤ 5⊢ 3 = 1 ∨ 3 = 5hm:4 ∣ 5hmle:4 ≤ 5⊢ 4 = 1 ∨ 4 = 5hm:5 ∣ 5hmle:5 ≤ 5⊢ 5 = 1 ∨ 5 = 5 hm:0 ∣ 5hmle:0 ≤ 5⊢ 0 = 1 ∨ 0 = 5 All goals completed! 🐙 hm:1 ∣ 5hmle:1 ≤ 5⊢ 1 = 1 ∨ 1 = 5 All goals completed! 🐙 hm:2 ∣ 5hmle:2 ≤ 5⊢ 2 = 1 ∨ 2 = 5 All goals completed! 🐙 hm:3 ∣ 5hmle:3 ≤ 5⊢ 3 = 1 ∨ 3 = 5 All goals completed! 🐙 hm:4 ∣ 5hmle:4 ≤ 5⊢ 4 = 1 ∨ 4 = 5 All goals completed! 🐙 hm:5 ∣ 5hmle:5 ≤ 5⊢ 5 = 1 ∨ 5 = 5 All goals completed! 🐙 private def polyFive (coeffs : Array Nat) : FpPoly 5 := ofCoeffs (coeffs.map (fun n => ZMod64.ofNat 5 n)) private def coeffNats (f : FpPoly 5) : List Nat := f.toArray.toList.map ZMod64.toNat private def sfFactorFive (coeffs : Array Nat) (multiplicity : Nat) : SquareFreeFactor 5 := { factor := polyFive coeffs, multiplicity } private def sfSummary (d : SquareFreeDecomposition 5) : Nat × List (List Nat × Nat) := (d.unit.toNat, d.factors.map (fun sf => (coeffNats sf.factor, sf.multiplicity))) private def sfReconstruction (d : SquareFreeDecomposition 5) : FpPoly 5 := DensePoly.C d.unit * weightedProduct d.factors -- Monic modulus x² + 2 over F₅, with x² ≡ 3. private def quadModulus : FpPoly 5 := { coeffs := #[(2 : ZMod64 5), 0, 1] normalized := ⊢ DensePolyNormalized #[2, 0, 1] ⊢ #[2, 0, 1].back? ≠ some Zero.zero ⊢ some 1 ≠ some 0 All goals completed! 🐙 } private theorem quadModulus_monic : DensePoly.Monic quadModulus := ⊢ DensePoly.Monic quadModulus All goals completed! 🐙 -- Monic linear modulus x + 3 over F₅. private def linearModulus : FpPoly 5 := { coeffs := #[(3 : ZMod64 5), 1] normalized := ⊢ DensePolyNormalized #[3, 1] ⊢ #[3, 1].back? ≠ some Zero.zero ⊢ some 1 ≠ some 0 All goals completed! 🐙 } private theorem linearModulus_monic : DensePoly.Monic linearModulus := ⊢ DensePoly.Monic linearModulus All goals completed! 🐙 -- (x + 1)³ mod (x² + 2) ≡ x. #guard coeffNats (powModMonic (polyFive #[1, 1]) quadModulus quadModulus_monic 3) = [0, 1] -- Exponent zero is the quotient-ring identity 1. #guard coeffNats (powModMonic (polyFive #[0, 0, 1]) quadModulus quadModulus_monic 0) = [1] -- Frobenius generator X⁵ mod (x² + 2) ≡ 4x. #guard coeffNats (frobeniusXMod quadModulus quadModulus_monic) = [0, 4] -- X⁵ mod (x + 3) ≡ 2, a constant. #guard coeffNats (frobeniusXMod linearModulus linearModulus_monic) = [2] -- frobeniusXPowMod _ _ 0 reduces X. #guard coeffNats (frobeniusXPowMod quadModulus quadModulus_monic 0) = [0, 1] -- Compose (3 + 2x + x²) with (1 + x) mod (x² + 2). #guard coeffNats (composeModMonic (polyFive #[3, 2, 1]) (polyFive #[1, 1]) quadModulus quadModulus_monic) = [4, 4] -- The weighted product of (x + 1)² is x² + 2x + 1. #guard coeffNats (weightedProduct [sfFactorFive #[1, 1] 2]) = [1, 2, 1] -- The empty product is the constant 1. #guard coeffNats (weightedProduct ([] : List (SquareFreeFactor 5))) = [1] -- Square-free decomposition: x² + 2x + 1 = (x + 1)². #guard sfSummary (squareFreeDecomposition prime_five (polyFive #[1, 2, 1])) = (1, [([1, 1], 2)]) -- The decomposition reconstructs its input. #guard let f := polyFive #[1, 2, 1] coeffNats (sfReconstruction (squareFreeDecomposition prime_five f)) = coeffNats f end HexPolyFpChapterExample