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.
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) : TypeHex.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
unconditional field instance. Instead the field-promoting laws are theorems that
take Hex.FpPoly.Irreducible of 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.
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
local instance boundsFive : ZMod64.Bounds 5 :=
⟨⊢ 0 < 5 All goals completed! 🐙, ⊢ 5 < 2 ^ 31 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 coeffNats (f : FpPoly 5) : List Nat :=
f.toArray.toList.map ZMod64.toNat
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 :=
.C d.unit * weightedProduct d.factors
-- Monic modulus x² + 2 over F₅, with x² ≡ 3.
private def quadModulus : FpPoly 5 := #p[2, 0, 1]
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 := #p[3, 1]
private theorem linearModulus_monic :
DensePoly.Monic linearModulus := ⊢ DensePoly.Monic linearModulus All goals completed! 🐙
-- (x + 1)³ mod (x² + 2) ≡ x.
#guard
coeffNats
(powModMonic #p[1, 1] quadModulus
quadModulus_monic 3) = [0, 1]
-- Exponent zero is the quotient-ring identity 1.
#guard
coeffNats
(powModMonic #p[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 #p[3, 2, 1] #p[1, 1]
quadModulus quadModulus_monic)
= [4, 4]
-- The weighted product of (x + 1)² is x² + 2x + 1.
#guard
coeffNats
(weightedProduct
[{ factor := #p[1, 1], multiplicity := 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
#p[1, 2, 1])
= (1, [([1, 1], 2)])
-- The decomposition reconstructs its input.
#guard
let f : FpPoly 5 := #p[1, 2, 1]
coeffNats
(sfReconstruction
(squareFreeDecomposition prime_five f))
= coeffNats f
end HexPolyFpChapterExample