hex

7.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.

7.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 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 instance : ZMod64.PrimeModulus 5 := ⟨prime_five⟩ /-- Monic degree-4 polynomial x⁴ + 2 over F₅. -/ private def modulus : FpPoly 5 := #p[2, 0, 0, 0, 1] private theorem modulus_pos_degree : 0 < FpPoly.degree modulus := ⊢ 0 < modulus.degree All goals completed! 🐙 private def q (f : FpPoly 5) : PolyQuotient modulus modulus_pos_degree := ofPoly modulus modulus_pos_degree f 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 #p[2, 3] private def b : PolyQuotient modulus modulus_pos_degree := q #p[4, 1, 0, 1] private def x : PolyQuotient modulus modulus_pos_degree := q #p[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