hex

8.6. Key correctness theorems🔗

Each ring operation is pinned down by a representativity law: its result is the residue of the corresponding Nat operation on the representatives, reduced modulo p. These are the lemmas downstream proofs rewrite with.

🔗theorem
Hex.ZMod64.toNat_add {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) : (a.add b).toNat = (a.toNat + b.toNat) % p
Hex.ZMod64.toNat_add {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  (a.add b).toNat =
    (a.toNat + b.toNat) % p

Addition agrees with addition of canonical representatives modulo p.

🔗theorem
Hex.ZMod64.toNat_sub {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) : (a.sub b).toNat = (a.toNat + (p - b.toNat)) % p
Hex.ZMod64.toNat_sub {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  (a.sub b).toNat =
    (a.toNat + (p - b.toNat)) % p

Subtraction agrees with modular subtraction of canonical representatives.

🔗theorem
Hex.ZMod64.toNat_mul {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) : (a.mul b).toNat = a.toNat * b.toNat % p
Hex.ZMod64.toNat_mul {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  (a.mul b).toNat = a.toNat * b.toNat % p

Multiplication agrees with multiplication of canonical representatives modulo p.

🔗theorem
Hex.ZMod64.toNat_pow {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p)
  (n : ℕ) : (a.pow n).toNat = a.toNat ^ n % p
Hex.ZMod64.toNat_pow {p : ℕ}
  [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p)
  (n : ℕ) :
  (a.pow n).toNat = a.toNat ^ n % p

Exponentiation agrees with natural-power reduction of the canonical representative.

Inversion is characterised on the elements where it is meaningful: a residue coprime to the modulus is a unit, with the computed inverse as its two-sided inverse.

🔗theorem
Hex.ZMod64.inv_mul_eq_one_of_coprime {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) (hcop : a.toNat.Coprime p) :
  a.inv.mul a = Hex.ZMod64.one
Hex.ZMod64.inv_mul_eq_one_of_coprime
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p)
  (hcop : a.toNat.Coprime p) :
  a.inv.mul a = Hex.ZMod64.one

Coprime residues multiply by their computed inverse to the unit residue.

Over a prime modulus the residues form a field. Under the Hex.ZMod64.PrimeModulus assumption (equivalently, a proof that p is prime) there are no zero divisors, every nonzero residue is invertible, and Fermat's little theorem holds.

🔗theorem
Hex.ZMod64.eq_zero_or_eq_zero_of_mul_eq_zero {p : ℕ}
  [Hex.ZMod64.Bounds p] (hp : Hex.Nat.Prime p) {a b : Hex.ZMod64 p}
  (h : a * b = 0) : a = 0 ∨ b = 0
Hex.ZMod64.eq_zero_or_eq_zero_of_mul_eq_zero
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p)
  {a b : Hex.ZMod64 p} (h : a * b = 0) :
  a = 0 ∨ b = 0

Prime-modulus residues have no zero divisors: if a * b = 0, then one of the factors is already zero.

🔗theorem
Hex.ZMod64.inv_mul_eq_one_of_prime {p : ℕ} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p) {a : Hex.ZMod64 p} (ha : a ≠ 0) : a.inv * a = 1
Hex.ZMod64.inv_mul_eq_one_of_prime {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p)
  {a : Hex.ZMod64 p} (ha : a ≠ 0) :
  a.inv * a = 1

Nonzero residues modulo a prime have multiplicative inverses.

🔗theorem
Hex.ZMod64.pow_prime {p : ℕ} [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p) (a : Hex.ZMod64 p) : a ^ p = a
Hex.ZMod64.pow_prime {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (hp : Hex.Nat.Prime p)
  (a : Hex.ZMod64 p) : a ^ p = a

Fermat's little theorem for ZMod64: raising a residue mod a prime p to the pth power returns the original residue.