Chapter 31 — Number-Theoretic Algorithms

Chapter 31 of CLRS covers algorithms for number theory: divisibility, the greatest common divisor, modular arithmetic, primality testing, and cryptography. This chapter formalizes all nine sections with the division theorem, Bezout's identity, the EUCLID / EXTENDED-EUCLID algorithms, the Chinese remainder theorem, Fermat's and Euler's theorems, RSA, the Fermat primality test, and the Pollard's-rho factorization heuristic.

Sections

31.1 Elementary Number-Theoretic Notions

• CLRS.Chapter31.division_theorem (Theorem 31.1) — division with a unique quotient and remainder.

• CLRS.Chapter31.IsGCD / CLRS.Chapter31.nat_gcd_isGCD — the greatest-common-divisor property.

• CLRS.Chapter31.divides_refl … CLRS.Chapter31.divides_sub (Lemma 31.1), and CLRS.Chapter31.exists_prime_ge (Euclid's theorem).

31.2 Greatest Common Divisor

• CLRS.Chapter31.euclid_recursion (Theorem 31.9, the GCD recursion theorem), CLRS.Chapter31.euclid + CLRS.Chapter31.euclid_eq_gcd, CLRS.Chapter31.gcd_is_linear_combination (Lemma 31.3, Bezout), CLRS.Chapter31.gcd_is_smallest_positive_linear_combination (Theorem 31.2), the Corollary 31.3/31.4 facts, and CLRS.Chapter31.extendedEuclid + extendedEuclid_spec.

• Running time (Lamé / Fibonacci): CLRS.Chapter31.euclidDivisions uses the second-argument CLRS convention. The actual CLRS.Chapter31.euclidWithCount follows the public first-argument recursion; CLRS.Chapter31.euclidWithCount_spec proves its count is euclidDivisions b a on the call euclid a b; CLRS.Chapter31.fib_le_of_euclidDivisions (Lemma 31.10) gives a ≥ F_{k+2}, b ≥ F_{k+1} for k calls; CLRS.Chapter31.euclidDivisions_lt (Theorem 31.11, Lamé) bounds the call count by b < F_{k+1}; and CLRS.Chapter31.euclidDivisions_le_two_log (Corollary 31.12) is the O(log b) bound.

31.3 Modular Arithmetic

• CLRS.Chapter31.mod_add / mod_mul (Theorem 31.5), CLRS.Chapter31.exists_mul_inverse_mod (Theorem 31.6), CLRS.Chapter31.mul_left_cancel_mod (Theorem 31.9), and CLRS.Chapter31.modular_linear_solvable (Corollary 31.21).

31.4 Solving Modular Linear Equations

• CLRS.Chapter31.linear_congruence_shift and CLRS.Chapter31.linear_congruence_all_solutions: the solutions of a·x ≡ b (mod n) are x₀ + k·(n/gcd(a,n)).

31.5 The Chinese Remainder Theorem

• CLRS.Chapter31.chinese_remainder_two, CLRS.Chapter31.chinese_remainder_unique, and CLRS.Chapter31.chinese_remainder (Theorem 31.27, two moduli).

31.6 Powers of an Element

• CLRS.Chapter31.modularExponentiation + modularExponentiation_spec, CLRS.Chapter31.fermat_little_theorem (Theorem 31.31), and CLRS.Chapter31.euler_theorem.

31.7 The RSA Public-Key Cryptosystem

• CLRS.Chapter31.totient_mul_prime and CLRS.Chapter31.rsa_correct (Theorem 31.36).

• CLRS.Chapter31.rsaKeyGen_roundTrip_mod and CLRS.Chapter31.rsaKeyGen_roundTrip connect generated keys to actual encryption/decryption for every message, with exact recovery below the modulus. Keys are assembled from supplied distinct primes; no prime generation, security, or key-assembly runtime is claimed.

31.8 Primality Testing

• CLRS.Chapter31.fermat_test (Theorem 31.31), CLRS.Chapter31.fermatPseudoprime, and CLRS.Chapter31.pseudoprime + pseudoprime_correct.

• Carmichael numbers: CLRS.Chapter31.isCarmichael — a composite n passing the Fermat test for every coprime base (CLRS.Chapter31.carmichael_fermatPseudoprime); CLRS.Chapter31.isCarmichael_561 proves that 561 is one; minimality is not proved.

• Miller-Rabin: CLRS.Chapter31.strongTestParams (the 2^s·d decomposition), CLRS.Chapter31.strongPseudoprime (STRONG-PSEUDOPRIME), CLRS.Chapter31.Witness, and the executable CLRS.Chapter31.millerRabin test. Correctness: CLRS.Chapter31.strongPseudoprime_of_prime (a prime passes every coprime base), CLRS.Chapter31.not_witness_of_prime, and CLRS.Chapter31.witness_not_prime (a witness certifies compositeness).

• Miller-Rabin error bound (Rabin–Monier): CLRS.Chapter31.goodUnits (S(n), the good subgroup), CLRS.Chapter31.liar_mem_goodSet (every strong liar lies in S(n)), and the counting machinery (CLRS.Chapter31.card_pow_eq_one_crt, CLRS.Chapter31.mTorsion_le_prod_half). The bound CLRS.Chapter31.goodUnits_card_le proves |S(n)| ≤ (n−1)/4 (three cases: prime power, semiprime, and ≥3 prime factors), giving CLRS.Chapter31.strongLiars_card_le — at most (n−1)/4 of the bases are strong liars (Theorem 31.39, sharpened to (n−1)/4 by Rabin–Monier).

• CLRS.Chapter31.MillerRabinExecution.run decides from counted residues and stops at the first rejecting base. Its counter is at most three times the number of supplied bases times Nat.size (n - 1) modular multiplications; decomposition, comparisons, sampling and bit runtime are excluded. CLRS.Chapter31.MillerRabinExecution.uniform_error_le proves the 4^-rounds executed error bound for the finite product of independent uniform nonzero residues. The old millerRabinLoop retains a detached budget.

31.9 Integer Factorization

⚠️ CLRS 4th edition removed this section (integer factorization is no

longer in the main text of Chapter 31). The POLLARD-RHO formalization is

retained for reference; a repo-wide migration will decide its fate.

• CLRS.Chapter31.rhoStep and CLRS.Chapter31.rho_collision_factor (Pollard's rho).

• POLLARD-RHO: CLRS.Chapter31.RhoState (tortoise-and-hare state), CLRS.Chapter31.pollardStep, the loop CLRS.Chapter31.pollardRhoLoop, and the full CLRS.Chapter31.pollardRho algorithm, with soundness CLRS.Chapter31.pollardRho_sound (a returned factor is a nontrivial divisor of n) and collision detection CLRS.Chapter31.pollardStep_collision_factor.

• Probabilistic analysis (CLRS Theorem 31.40): the rho-orbit-read-mod-p heuristic is made an explicit i.i.d.-uniform model (Fin k → Fin p), with the birthday bound CLRS.Chapter31.birthday_noCollision_le / CLRS.Chapter31.birthday_collision_ge / CLRS.Chapter31.birthday_collision_prob_ge_half, the expected-O(√p) bound CLRS.Chapter31.rho_expected_rounds_le_two / CLRS.Chapter31.rho_expected_draws_le, and the detection lemmas CLRS.Chapter31.pollardStep_detects / CLRS.Chapter31.pollardRhoLoop_terminates_on_collision bound to the real construction.

Status: main-proof-complete for the represented mathematical interfaces of Sections 31.1–31.8. The legacy §31.9 integer-factorization material remains in the online scope.

Cost and implementation boundaries

The executable interfaces include the modular equation solver, counted modular exponentiation, supplied-prime RSA key assembly and round trips, and the residue-based Miller–Rabin loop. Euclid counts division steps; exponentiation and Miller–Rabin count modular multiplications. These are not bit-runtime claims. Miller–Rabin parameter decomposition, comparisons and base sampling are uncounted, and the old loop retains a detached budget. RSA key-prime generation, key-assembly runtime and security are outside the proved interface. The finite-product Miller–Rabin error theorem assumes independent uniform bases with replacement from nonzero residues.