hex

14.3. Principal operations🔗

Ring operations on Hex.GFqRing.PolyQuotient lift the corresponding operations on representatives and re-reduce the result.

🔗def
Hex.GFqRing.zero {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) : Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.zero {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) :
  Hex.GFqRing.PolyQuotient f hf

The quotient zero element.

🔗def
Hex.GFqRing.one {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) : Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.one {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) :
  Hex.GFqRing.PolyQuotient f hf

The quotient one element.

🔗def
Hex.GFqRing.const {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (c : Hex.ZMod64 p) : Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.const {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (c : Hex.ZMod64 p) :
  Hex.GFqRing.PolyQuotient f hf

Embed a prime-field constant as a quotient-ring constant polynomial.

🔗def
Hex.GFqRing.add {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (x y : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.add {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree}
  (x y : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf

Quotient addition reduces the sum of representatives.

🔗def
Hex.GFqRing.mul {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (x y : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.mul {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree}
  (x y : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf

Quotient multiplication reduces the product of representatives.

🔗def
Hex.GFqRing.neg {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.neg {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree}
  (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf

Quotient negation reduces the coefficientwise additive inverse.

🔗def
Hex.GFqRing.sub {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (x y : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.sub {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree}
  (x y : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf

Quotient subtraction reduces the difference of representatives.

🔗def
Hex.GFqRing.pow {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (x : Hex.GFqRing.PolyQuotient f hf) (n : Nat) :
  Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.pow {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree}
  (x : Hex.GFqRing.PolyQuotient f hf)
  (n : Nat) :
  Hex.GFqRing.PolyQuotient f hf

Quotient exponentiation by square-and-multiply on the exponent bits, costing O(log n) quotient-ring multiplications.

Exponentiation uses square-and-multiply on the exponent bits, costing O(log n) quotient-ring multiplications. The natural and integer scalar maps below use the same binary-decomposition shape. The textbook n + 1 ↦ pred + 1 recursion is forbidden in this library because its cost would be linear in the scalar.

🔗def
Hex.GFqRing.natCast {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (n : Nat) : Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.natCast {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (n : Nat) :
  Hex.GFqRing.PolyQuotient f hf

Natural-number literals in the quotient ring are reduced constant polynomials.

🔗def
Hex.GFqRing.nsmul {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (n : Nat) (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.nsmul {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (n : Nat)
  (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf

Natural scalar multiplication in the quotient ring.

🔗def
Hex.GFqRing.intCast {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) : Int → Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.intCast {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) :
  Int → Hex.GFqRing.PolyQuotient f hf

Integer literals in the quotient ring.

🔗def
Hex.GFqRing.zsmul {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (i : Int) (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.zsmul {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (i : Int)
  (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqRing.PolyQuotient f hf

Integer scalar multiplication in the quotient ring.

The standard typeclass instances Zero, One, Add, Mul, Neg, Sub, and Pow on Hex.GFqRing.PolyQuotient are defined by the corresponding operations above, so ring-literal notation such as 0, 1, x + y, x * y, -x, x - y, and x ^ n works over PolyQuotient f hf out of the box.

14.3.1. Worked example: F₅ modulo x⁴ + 2🔗

The reduction rule for this quotient is x⁴ ≡ -2 ≡ 3 (mod 5). The example below builds the modulus, three reduced representatives a, b, and x, then runs addition, multiplication, negation, subtraction, and exponentiation.

open Hex Hex.GFqRing namespace HexGFqRingChapterExample private instance : ZMod64.Bounds 5 := ⟨⊢ 0 < 5 All goals completed! 🐙, ⊢ 5 ≤ UInt64.word 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 instance : ZMod64.PrimeModulus 5 := ⟨prime_five⟩ private theorem one_ne_zero_five : (1 : ZMod64 5) ≠ 0 := ⊢ 1 ≠ 0 h:1 = 0⊢ False h:1 = 0this:1 % 5 = 0 % 5⊢ False All goals completed! 🐙 /-- Monic degree-4 polynomial x⁴ + 2 over F₅. -/ private def modulus : FpPoly 5 := { coeffs := #[(2 : ZMod64 5), 0, 0, 0, 1] normalized := ⊢ DensePolyNormalized #[2, 0, 0, 0, 1] ⊢ #[2, 0, 0, 0, 1].back? ≠ some Zero.zero ⊢ some 1 ≠ some 0 All goals completed! 🐙 } private theorem modulus_pos_degree : 0 < FpPoly.degree modulus := ⊢ 0 < modulus.degree All goals completed! 🐙 private def q (coeffs : Array Nat) : PolyQuotient modulus modulus_pos_degree := ofPoly modulus modulus_pos_degree (FpPoly.ofCoeffs (coeffs.map (fun n => ZMod64.ofNat 5 n))) private def reprNats (x : PolyQuotient modulus modulus_pos_degree) : List Nat := (repr x).toArray.toList.map ZMod64.toNat private def a : PolyQuotient modulus modulus_pos_degree := q #[2, 3] private def b : PolyQuotient modulus modulus_pos_degree := q #[4, 1, 0, 1] private def x : PolyQuotient modulus modulus_pos_degree := q #[0, 1] -- (2 + 3x) + (4 + x + x³) ≡ 1 + 4x + x³ (mod 5) #guard reprNats (a + b) = [1, 4, 0, 1] -- (2 + 3x)(4 + x + x³) reduced through x⁴ ≡ 3. #guard reprNats (a * b) = [2, 4, 3, 2] -- -(2 + 3x) ≡ 3 + 2x (mod 5) #guard reprNats (-a) = [3, 2] -- (2 + 3x) - (4 + x + x³) ≡ 3 + 2x + 4x³ (mod 5) #guard reprNats (a - b) = [3, 2, 0, 4] -- Powers of x exercising x⁴ ≡ 3. #guard reprNats (x ^ 3) = [0, 0, 0, 1] #guard reprNats (x ^ 4) = [3] #guard reprNats (x ^ 5) = [0, 3] end HexGFqRingChapterExample