4.2. Symmetric representatives🔗

An integer x with |x| < m / 2 is determined by its residue modulo m: it is the representative of the residue in the interval (-m/2, m/2]. So reconstructions in this library return that representative rather than the usual one in [0, m), and negative answers come out negative.

def

Hex.Modular.symMod (a : ℤ) (m : ℕ) : ℤ
Hex.Modular.symMod (a : ℤ) (m : ℕ) : ℤ

The representative of a modulo m in the interval (-m/2, m/2]. For the degenerate modulus zero, this returns a, matching Int.emod's zero-modulus convention.

[-3, 5, 5]#eval [symMod 17 10, symMod 15 10, symMod (-15) 10]

[-3, 5, 5]

The uniqueness theorem needs the strict inequality 2 |x| < m. When m is even, m / 2 and -m / 2 have the same residue, and the interval keeps only the first of them:

theorem

Hex.Modular.symMod_unique {a x : ℤ} {m : ℕ} (h : 2 * x.natAbs < m)
  (hx : x % ↑m = a % ↑m) : Hex.Modular.symMod a m = x
Hex.Modular.symMod_unique {a x : ℤ}
  {m : ℕ} (h : 2 * x.natAbs < m)
  (hx : x % ↑m = a % ↑m) :
  Hex.Modular.symMod a m = x

A strictly-half-bounded integer congruent to a is the unique symmetric representative. The strict bound excludes the two representatives at an even tie.