4.3.1. Garner's step🔗

Suppose the state holds v modulo M, and r modulo m is pushed, with M and m coprime. Let s be the inverse of M modulo m. Then δ = symMod ((r - v) s) m and the new value is symMod (v + M δ) (M m). Adding a multiple of M does not change the residue modulo M, and modulo m the sum is v + (r - v) = r. This is Garner's mixed-radix step. The inverse s comes from the extended Euclidean algorithm applied to M mod m and m, so its operands are no larger than m, whatever the size of M. When m fits in a word, the other operations (additions, multiplications by numbers smaller than m, and reductions) each take time linear in the bit length of M.

The final reduction is needed. Pushing 1 mod 3 and then 0 mod 2 gives δ = 1 and v + M δ = 4, which is outside (-3, 3]; the stored value is -2:

some (-2, 6)

Three theorems describe a successful push. The new modulus is the product, the new value has the new residue, and it keeps the old residue modulo every divisor of the old modulus. By induction, the value after a sequence of pushes has every residue that was pushed.

Hex.Modular.Crt.push_modulus {c c' : Hex.Modular.Crt} {r : ℤ} {m : ℕ}
  (h : c.push r m = some c') : c'.modulus = c.modulus * m
Hex.Modular.Crt.push_modulus
  {c c' : Hex.Modular.Crt} {r : ℤ} {m : ℕ}
  (h : c.push r m = some c') :
  c'.modulus = c.modulus * m

Hex.Modular.Crt.push_congr_new {c c' : Hex.Modular.Crt} {r : ℤ} {m : ℕ}
  (h : c.push r m = some c') : c'.value % ↑m = r % ↑m
Hex.Modular.Crt.push_congr_new
  {c c' : Hex.Modular.Crt} {r : ℤ} {m : ℕ}
  (h : c.push r m = some c') :
  c'.value % ↑m = r % ↑m

Hex.Modular.Crt.push_congr_old {c c' : Hex.Modular.Crt} {r : ℤ}
  {m d : ℕ} (hd : d ∣ c.modulus) (h : c.push r m = some c') :
  c'.value % ↑d = c.value % ↑d
Hex.Modular.Crt.push_congr_old
  {c c' : Hex.Modular.Crt} {r : ℤ}
  {m d : ℕ} (hd : d ∣ c.modulus)
  (h : c.push r m = some c') :
  c'.value % ↑d = c.value % ↑d

To recover an integer x, push residues of x until 2 |x| is less than the modulus. The value then has the same residue as x modulo the whole modulus, and it is the symmetric representative of that residue, so it is x by symMod_unique. The same argument gives the uniqueness of strictly bounded solutions:

Hex.Modular.crt_unique {c : Hex.Modular.Crt} {x y : ℤ}
  (h : 2 * x.natAbs < c.modulus) (h' : 2 * y.natAbs < c.modulus)
  (hx : x % ↑c.modulus = y % ↑c.modulus) : x = y
Hex.Modular.crt_unique
  {c : Hex.Modular.Crt} {x y : ℤ}
  (h : 2 * x.natAbs < c.modulus)
  (h' : 2 * y.natAbs < c.modulus)
  (hx : x % ↑c.modulus = y % ↑c.modulus) :
  x = y

4.3.2. Vectors of residues🔗

Recovering a polynomial or a matrix means recovering many integers modulo the same primes. A CrtVec k (Hex.Modular.CrtVec) holds k values sharing one modulus. Its Hex.Modular.CrtVec.push computes the inverse s once and uses it for every coordinate, so a push costs one extended Euclidean algorithm whatever k is. Here the second coordinate solves 1 mod 3, 0 mod 5 and -1 mod 7:

some (#v[23, -50], 105)

CrtVec has the same theorems as Crt, for every coordinate, together with Hex.Modular.CrtVec.push_congr, which combines the old and new residues into one congruence modulo the product, and Hex.Modular.CrtVec.eq_of_congr, the analogue of crt_unique.

4.3.3. Many moduli at once🔗

When every modulus is known before any residue, the moduli can be prepared once and used for many reconstructions. Hex.Modular.CrtPlan.build? checks that the moduli are greater than one and pairwise coprime, and arranges them as the leaves of a balanced binary tree. Each internal node stores the inverse of the product of its left subtree modulo the product of its right subtree. Hex.Modular.CrtPlan.reconstruct? then combines the residues from the leaves up, applying Garner's step at each node with its stored inverse, so it runs no extended Euclidean algorithm. Hex.Modular.CrtPlan.reconstructVec? does the same for k values at once: its input is an Array (Vector Int k) with one vector of residues per modulus, in the order of the moduli, and it uses each stored inverse for every coordinate. Both return none if the number of residues differs from the number of moduli, and both check the result against every residue before returning it.

A plan for the five primes above recovers the same residue of H₅₀ as the incremental computation:

The result is the symmetric representative modulo the product of the moduli, so it recovers every integer that small:

Hex.Modular.CrtPlan.reconstruct?_eq_candidate
  {plan : Hex.Modular.CrtPlan} {residues : Array ℤ}
  {value candidate : ℤ}
  (hresult : plan.reconstruct? residues = some value)
  (hbound : 2 * candidate.natAbs < plan.modulus)
  (hcongr :
    ∀ (i : Fin plan.moduli.size),
      candidate % ↑plan.moduli[i] =
        residues.getD (↑i) 0 % ↑plan.moduli[i]) :
  value = candidate
Hex.Modular.CrtPlan.reconstruct?_eq_candidate
  {plan : Hex.Modular.CrtPlan}
  {residues : Array ℤ}
  {value candidate : ℤ}
  (hresult :
    plan.reconstruct? residues =
      some value)
  (hbound :
    2 * candidate.natAbs < plan.modulus)
  (hcongr :
    ∀ (i : Fin plan.moduli.size),
      candidate % ↑plan.moduli[i] =
        residues.getD (↑i) 0 %
          ↑plan.moduli[i]) :
  value = candidate

The incremental form is the one to use when the number of moduli is not known in advance, because a computation can stop as soon as it has enough. The section Costs and limits compares the two.