Choosing coprime moduli at the desired scale

As in Lecomte and Ramakrishnan, Section 4, use the smallest power of each of the first r primes that exceeds the integer scale k. These powers lie between k and a constant (depending only on r) times k.

theorem Complexity.Shallow.exists_moduli (r : ℕ) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (k : ℕ), 1 ≤ k → ∃ (m : Fin r → ℕ), (Pairwise fun (i j : Fin r) => (m i).Coprime (m j)) ∧ (∀ (i : Fin r), k < m i) ∧ ∀ (i : Fin r), m i ≤ C * k

Any fixed number of pairwise coprime moduli can be chosen at a common scale, with constants independent of that scale.

theorem Complexity.Shallow.pow_lt_prod_moduli {r k : ℕ} (hr : 0 < r) (m : Fin r → ℕ) (hm : ∀ (i : Fin r), k < m i) : k ^ r < ∏ i : Fin r, m i

The product of r moduli exceeding k exceeds k^r.