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 counts the recursive calls of EUCLID; 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).

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 exhibits the smallest one.

• 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 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).

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: selected-section-complete — Sections 31.1–31.9 fully proved, including the Miller-Rabin error bound and the POLLARD-RHO probabilistic analysis (birthday bound + expected O(√p)).

Deferred Work

The remaining scope outside the represented fourth-edition sections is the RSA security (one-way function) claim and the ZMod.chineseRemainder ring-isomorphism packaging. The executable layers are now complete: modularLinearEquationSolver (§31.4), modExpWithCount (§31.6), rsaKeyGen/rsaEncrypt/rsaDecrypt (§31.7), and millerRabinLoop (§31.8). The legacy §31.9 integer-factorization development is retained as online material with its probabilistic analysis complete.