feat(ch31): complete the Miller-Rabin error bound (Theorem 31.39, 4th ed.) - #155
Open
TankTechnology wants to merge 25 commits into
Open
feat(ch31): complete the Miller-Rabin error bound (Theorem 31.39, 4th ed.)#155TankTechnology wants to merge 25 commits into
TankTechnology wants to merge 25 commits into
Conversation
- 31.5 chinese_remainder_general: the full k-modulus Chinese remainder theorem via Nat.chineseRemainderOfList (existence + uniqueness mod the product). - 31.4 linear_congruence_solutions: the solutions of a·x ≡ b (mod n) are exactly the residue class x0 mod (n/gcd(a,n)) (Thm 31.10). - 31.4 linear_congruence_distinct: the d = gcd(a,n) values k·(n/d) for k < d are pairwise incongruent, so there are exactly d distinct solutions. Co-Authored-By: Claude <noreply@anthropic.com>
- rsa_pow_cong: for prime p and e*d ≡ 1 (mod p-1), m^(e*d) ≡ m (mod p) — covering both p|m and p∤m via ZMod.pow_card_sub_one. - rsa_correct_general: for distinct primes p q and e*d ≡ 1 (mod (p-1)(q-1)), m^(e*d) ≡ m (mod p*q) for every m, via the per-prime congruences and the Chinese remainder theorem. - prime_coprime: distinct primes are coprime. Co-Authored-By: Claude <noreply@anthropic.com>
Add the Fibonacci running-time analysis of the Euclidean algorithm,
closing the last 31.2 deferred item:
- euclidDivisions counts the recursive calls of CLRS EUCLID.
- fib_le_of_euclidDivisions (CLRS Lemma 31.10): k calls with a > b >= 1
force b >= F_{k+1} and a >= F_{k+2}, by strong induction on b.
- euclidDivisions_lt (CLRS Theorem 31.11, Lamé's theorem): b < F_{k+1}
implies fewer than k calls.
- euclidDivisions_le_two_log (CLRS Corollary 31.12): at most 2*log2 b + 2
calls, i.e. O(log b), via new exponential growth lemmas
fib_two_step_ge_pow_two / pow_two_le_fib (2^(n/2) <= F_{n+2}).
All theorems kernel-checked with clean axioms; progress CSV bumped to
22/22 tracked theorems and docs/proof-map.md updated.
Co-Authored-By: Claude <noreply@anthropic.com>
Add the Carmichael-number half of the 31.8 deferred work: - isCarmichael n: composite and a^(n-1) ≡ 1 (mod n) for every a coprime to n, with the projection lemmas and carmichael_fermatPseudoprime (a Carmichael number is a Fermat pseudoprime to every coprime base). - isCarmichael_561: the smallest Carmichael number is 561, shown via fermat_test for the prime factors 3, 11, 17 and the new helper modeq_of_coprime_mul (combining congruences under coprime moduli). This concretely shows PSEUDOPRIME cannot certify primality. Kernel-clean axioms; progress CSV bumped to 24/24 and docs updated. Co-Authored-By: Claude <noreply@anthropic.com>
Define the Miller-Rabin machinery (correctness/error bound deferred): - strongTestParams: write n-1 = 2^s * d with d odd via Nat.factorization. - strongPseudoprime (STRONG-PSEUDOPRIME): a^d ≡ 1 or a^(2^i * d) ≡ -1 for some i < s (i ranging over Fin s for decidability). - Witness: a base that refutes strong pseudoprimality. - millerRabin: the executable single-base decision procedure. - instDecidableStrongPseudoprime for the Fin-bounded search. Computational sanity checks: millerRabin 5 2 = true, 9 2 = false, and 561 2 = false - although 561 is a Carmichael number, base 2 witnesses that it is composite, illustrating why Miller-Rabin beats PSEUDOPRIME. Kernel-clean; docs and proof map updated; correctness/error bound remain deferred. Co-Authored-By: Claude <noreply@anthropic.com>
Prove the prime direction of Miller-Rabin correctness in 31.8: - strongTestParams_spec: the 2^s·d decomposition of n-1 (via Nat.Prime.pow_dvd_iff_le_factorization and Nat.mul_div_cancel'). - modeq_neg_one_of_sq_eq_one: for a prime p, x^2 ≡ 1 and x ≢ 1 (mod p) imply x ≡ -1 — the roots-of-unity fact via Nat.sq_sub_sq and Nat.Prime.dvd_mul. - strongPseudoprime_of_prime: for prime n and a coprime to n, the sequence a^d, a^(2d), ..., a^(2^s·d) reaches 1 (Fermat); at the first such index the previous value is a square root of 1 that is not 1, hence -1. Uses Nat.find for the minimal index. - not_witness_of_prime (a prime has no witness) and witness_not_prime (a witness certifies compositeness). Kernel-clean axioms; progress CSV bumped to 26/26; only the Miller-Rabin error bound and Pollard's-rho analysis remain deferred. Co-Authored-By: Claude <noreply@anthropic.com>
Complete the deterministic part of the 31.9 deferred work: - rho_collision_factor_dist: the |y-x| (Nat.dist) version of the collision-factor lemma, matching GCD(|y-x|, n) in POLLARD-RHO. - RhoState (tortoise-and-hare state: step count, current value, power-of-two snapshot, next boundary), pollardStep (one iteration), pollardRhoLoop (over a step budget), and pollardRho (the full CLRS algorithm). - pollardRho_sound: whenever the returned value differs from n it is a nontrivial divisor of n (the only exit producing a value is the 1 < d < n check on the gcd, and the gcd always divides n). - pollardStep_collision_factor: a mod-p collision at a step makes that step's candidate a multiple of p, so the loop returns a factor. Kernel-clean (pollardRho_sound needs only propext and Quot.sound); progress CSV bumped to 27/27. The birthday-paradox expected-O(sqrt p) running-time analysis remains deferred as a CLRS heuristic. Co-Authored-By: Claude <noreply@anthropic.com>
Start the error-bound proof with the clean foundational lemmas: - modeq_pow_two_sub_one: (n-1)^2 ≡ 1 (mod n), via (n-1)^2 - 1 = n*(n-2). - strongPseudoprime_pow: a strong probable prime to base a satisfies a^(n-1) ≡ 1 (mod n). With n-1 = 2^s·d, either a^d ≡ 1, or a^(2^i·d) ≡ -1 and a^(n-1) = (a^(2^i·d))^(2^(s-i)) ≡ (-1)^even = 1. Every strong liar therefore lies in the kernel of a ↦ a^(n-1), the first step toward showing the liars form a subgroup of the units. Kernel-clean axioms. Co-Authored-By: Claude <noreply@anthropic.com>
Co-Authored-By: Claude <noreply@anthropic.com>
Write docs/ch31-error-bound-handoff.md capturing the verified roadmap for
the last remaining ch31 theorem (Rabin-Monier: at most phi(n)/4 strong
liars for odd composite n). Key content:
- Correct structure: embed liars into the subgroup S(n) = {x :
x^(2^(nu(n)-1)*t) ≡ ±1 mod n}, then bound |S| ≤ phi(n)/4 via the
three-case analysis (>=3 prime factors, n=pq, n=p^2).
- Verified negative result: strong liars are NOT a subgroup for
multi-prime n (brute-force counterexamples 65/85/145/185), so the naive
subgroup approach is wrong; prime powers are cyclic.
- Mathlib gap: cyclicity of (Z/p^e)^* / exists_primitive_root is missing;
build it first (Milestone 0).
- Concrete Milestone 0-4 attack order and reusable API/lemma inventory.
Co-Authored-By: Claude <noreply@anthropic.com>
Add the verified Mathlib findings from the attack's first step: - Cyclicity of (Z/p)^* for prime p is a free instance (finite-field unit-group theorem), with IsCyclic.exists_generator as the generator. - (Z/p^e)^* cyclicity for e >= 2 is NOT in Mathlib; suggest either proving primitive roots mod odd prime powers or a Hensel-lifting reduction to (Z/p)^*. - Nat.card (ZMod n)^* = totient n is not a named lemma but the pieces exist (Nat.card_units, totient_eq_card_coprime). - Revised Milestone 0-4 order. Co-Authored-By: Claude <noreply@anthropic.com>
…ib gaps
Verified corrections to the Miller-Rabin error-bound handoff:
- Target ≤ (n−1)/4, NOT ≤ φ(n)/4: the φ-bound is false for n = 9
(liars(9) = {1,8}, 2 > φ(9)/4 = 1; (n−1)/4 gives equality).
- |S(n)| = 2^(k(ν−1)+1)·∏gcd(t,d_i) and exact liar count
|L| = G·(2^(kν)−1)/(2^k−1) re-derived and checked on n = 9,15,25,65,561.
- Both former "gaps" are now in Mathlib: ZMod.isCyclic_units_of_prime_pow
((Z/p^e)ˣ cyclic for odd p, no Hensel needed) and
ZMod.card_units_eq_totient (the φ-bridge). Only remaining primitive to
write: #{x : α // x^n = 1} = gcd(n, |α|) for cyclic α.
Co-Authored-By: Claude <noreply@anthropic.com>
…rs ⊆ S
Milestone 1-2 of the Rabin-Monier error bound. Kernel-clean (only
propext/Classical.choice/Quot.sound).
- units of ZMod n: Nat.card (ZMod n)ˣ = φ(n), prime case p−1.
- nu(n) = min over prime factors p of v₂(p−1), with 2^ν | p−1 and ν ≥ 1
for odd n.
- S(n) = {x ∈ (ZMod n)ˣ : x^(2^(ν−1)·t) ∈ {±1}} as a Subgroup (preimage of
{1,−1} under the power map), avoiding ZMod-coercion pain.
- Parity lemma: orderOf (a^(2^i·d)) = 2 with d odd ⟹ 2^(i+1) | orderOf a.
- liar_mem_goodSet: every strong liar lies in S(n), via reduction mod each
prime divisor (ZMod.castHom) + the parity lemma forcing 2^(i+1) | p−1.
Co-Authored-By: Claude <noreply@anthropic.com>
Milestone 3 foundation: the counting kernel for |S(n)|.
- card_multiples_dvd: #{i < N : d | i} = N/d for d | N.
- card_fin_dvd_mul: #{i < N : N | i·n} = gcd(N, n), via the gcd-reduction
(N/g | i) and coprimality of quotients.
- card_pow_eq_one_cyclic: in a finite cyclic group of order N, the number of
elements with x^n = 1 is gcd(n, N) — via the generator parametrization
(IsCyclic.image_range_card) and the i ↦ g^i bijection.
All kernel-clean (only propext/Classical.choice/Quot.sound).
Co-Authored-By: Claude <noreply@anthropic.com>
Milestone 3a: the per-prime-power counting primitive.
- card_pow_eq_one_prime_pow: #{x : (ZMod (p^e))ˣ // x^m = 1} = gcd(m, φ(p^e))
via cyclicity of (Z/p^e)ˣ (ZMod.isCyclic_units_of_prime_pow) + the cyclic
torsion count.
- card_pow_eq_c_of_exists: in a finite commutative group, the fiber of x↦x^m
over any element in its image has the same size as the m-torsion (coset of
the kernel).
- card_pow_le_card_pow_eq_one: so any fiber has size ≤ the m-torsion — this
bounds the "≡ −1" part by the "≡ 1" part without needing −1 in the image.
Kernel-clean (only propext/Classical.choice/Quot.sound).
Co-Authored-By: Claude <noreply@anthropic.com>
Milestone 3b: card_pow_eq_one_crt shows the number of units x modulo n with x^m = 1 equals the product over prime factors p of the number of units modulo p^e_p with x^m = 1. Uses ZMod.equivPi (the CRT as a ring isomorphism on ZMod n), Units.mapEquiv + MulEquiv.piUnits to lift to unit groups, and Equiv.subtypePiEquivPi to turn the pointwise-torsion subtype into a Pi of per-prime-power torsion subtypes. Kernel-clean (only propext/Classical.choice/Quot.sound). Co-Authored-By: Claude <noreply@anthropic.com>
…1)/2 Milestone 3c (partial): the key per-prime-factor bound for |S(n)|. - odd_dvd_of_dvd_mul_two / odd_of_dvd_odd: odd-divisor helpers. - gcd_pow_mul_le_half: for m = 2^(ν−1)·t with t odd and 2^ν | p−1, the gcd of m and p−1 is at most (p−1)/2 (2-adic valuation ≤ ν−1, odd part ≤ d). Kernel-clean (only propext/Classical.choice/Quot.sound). Co-Authored-By: Claude <noreply@anthropic.com>
Milestone 3 assembly: the structural bound for the error bound.
- card_subtype_filter, card_or_le: counting a disjunction of predicates.
- goodSet_card_le: |S(n)| = |{x : x^m ∈ {±1}}| ≤ 2·|{x : x^m = 1}| — the
"≡ −1" part is a fiber of the power map, no larger than the m-torsion.
- mTorsion_eq_prod: the m-torsion of (ZMod n)ˣ is the product over prime
factors p of gcd(m, φ(p^e_p)) (via card_pow_eq_one_crt + the per-prime-power
count).
Together: |S(n)| ≤ 2·∏ gcd(m, φ(p^e)) ≤ 2^(1−k)·∏(p−1). Kernel-clean.
Co-Authored-By: Claude <noreply@anthropic.com>
Completes the structural bound for the error bound: |S(n)| ≤ 2·|S₁| ≤ 2·∏(p−1)/2 = 2^(1−k)·∏(p−1). - nu_le_v2_nat_sub_one: ν(n) ≤ v₂(n−1), since every prime factor is ≡ 1 mod 2^ν and n = ∏p^e (Nat.ModEq.prod_one). - mExp_dvd: m = 2^(ν−1)·t divides n−1. - mExp_coprime_prime: m is coprime to every prime factor p of n. - gcd_eq_gcd_of_coprime / gcd_totient_eq_gcd_prime: gcd(m, φ(p^e)) = gcd(m, p−1). - mTorsion_le_prod_half: |S₁| ≤ ∏ (p−1)/2, via the per-factor gcd bound gcd_pow_mul_le_half. Kernel-clean (only propext/Classical.choice/Quot.sound). The remaining work is the three-case arithmetic (|S| ≤ 2^(1−k)·∏(p−1) ≤ (n−1)/4 for k ≥ 3, k = 1, k = 2). Co-Authored-By: Claude <noreply@anthropic.com>
Milestones 1-3 (ν, S(n), liars ⊆ S, |S| ≤ 2^(1−k)·∏(p−1)) are committed. The handoff now documents the only remaining work — Milestone 4, the three-case bound |S| ≤ (n−1)/4 — with the k=2 analysis worked out: - sub-case s < r is easy via pq−1 ≥ 2^(2ν+1)d_p·d_q (no d/gcd needed); - sub-case s = r needs "d_p | t ∧ d_q | t ⟹ d_p = d_q ⟹ p = q" to get a factor-3 saving. Co-Authored-By: Claude <noreply@anthropic.com>
Milestone 4 of the Rabin–Monier error-bound proof: the three-case arithmetic bound on the good subgroup S(n). - k=1 (prime power): |S| ≤ p−1 ≤ (p^e−1)/4 via the CRT m-torsion count and 4(p−1) ≤ p²−1. - k=2 (semiprime n = p^a q^b): squarefree n=pq uses the refined bound 8·gcd(m,p−1)·gcd(m,q−1) ≤ pq−1, split into s<r (2^(2s+1) ≤ 2^(s+r)) and s=r (key lemma: d_p|t ∧ d_q|t forces p=q, giving a factor-3 saving); non-squarefree uses the crude 2(p−1)(q−1) ≤ n−1. - k≥3: 2^(1−k)·∏(p−1) ≤ (n−1)/4 via ∏(p−1) ≤ n−1. Key lemmas: nu_semiprime (ν(pq) = min v₂(p−1) v₂(q−1)), gcd_pow_mul_oddPart (gcd decomposition), semiprime_key_lemma, semiprime_gcd_bound, crude_bound, prod_primeFactors_pair, goodUnits_card_le_semiprime. Assembles to goodUnits_card_le (|S(n)| ≤ (n−1)/4) and the headline strongLiars_card_le: at most (n−1)/4 of the bases are strong liars for odd composite n (Theorem 31.38). Kernel-clean: only propext/Classical.choice/Quot.sound, no sorryAx. Docs: chapter guide, progress CSV (29/29 tracked), proof map, and the module header all updated; the error bound is no longer deferred.
The project base is now the CLRS 4th edition, which renumbered several
results in Chapter 31. Verified against the 4th-edition text:
- Miller-Rabin error bound: Theorem 31.38 -> Theorem 31.39 (the
witnesses >= (n-1)/2 theorem; (n-1)/4 is its Rabin-Monier sharpening).
- Fermat's little theorem: Theorem 31.30 -> Theorem 31.31; Euler's
theorem is Theorem 31.30.
- Modular-linear solvability: Theorem 31.11 -> Corollary 31.21; the
distinct-solutions count is Corollary 31.22.
- Euclid recursion: Lemma 31.2 -> Theorem 31.9 (GCD recursion theorem).
- Fixed the handoff doc title typo ("Theorem 31.8" -> 31.39).
- Noted that the 4th edition removed Section 31.9 (integer
factorization); the POLLARD-RHO file is retained pending the repo-wide
migration.
The §31.1-31.3 references (mod_add, exists_mul_inverse_mod,
mul_left_cancel_mod, gcd_is_linear_combination) remain on their legacy
numbers pending the repo-wide 4th-edition migration.
Co-Authored-By: Claude <noreply@anthropic.com>
TankTechnology
changed the title
Bring origin/main (37 commits: 4th-edition facade, edition maps, Ch30, literate shard infrastructure, scripts) into feat/ch31-refinements. The ch31 section files merged cleanly, keeping the full Miller-Rabin error-bound work (strongLiars_card_le). Conflicts resolved only in CLRSLean/Progress.lean and docs/clrs-proof-progress.csv, taking the remote's new fourth-edition schema. Verification: lake build CLRSLean (8958 jobs) passes; check_repository.py and check_progress_csv.py (1326/1326) pass. Co-Authored-By: Claude <noreply@anthropic.com>
Add goodUnits_card_le and strongLiars_card_le to the chapter 31 row of the fourth-edition progress ledger (tracked/proved 15 -> 17), since the merged error-bound work is now in the source. Regenerate Progress.lean and the README progress table; update the snapshot test's expected total (1,326 -> 1,328). Co-Authored-By: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Completes the last remaining hard theorem in Chapter 31: the Rabin–Monier
error bound — at most
(n−1)/4of the bases are strong liars for oddcomposite
n.What this PR proves
CLRS.Chapter31.strongLiars_card_le— the headline theorem. It followsfrom
goodUnits_card_le, which bounds the good subgroupS(n)by threecases on the number of distinct prime factors:
n = p^e):|S| ≤ p−1 ≤ (p^e−1)/4.n = p^a q^b): squarefreen = pquses the refined8·gcd(m,p−1)·gcd(m,q−1) ≤ pq−1, split intos < rands = r; thelatter needs the key lemma
d_p | t ∧ d_q | t ⟹ p = q. Non-squarefreeuses the crude
2(p−1)(q−1) ≤ n−1.2^(1−k)·∏(p−1) ≤ (n−1)/4.Verification
lake build CLRSLeanpasses (8900 jobs).#print axioms strongLiars_card_le/goodUnits_card_leshow onlypropext,Classical.choice,Quot.sound— nosorryAx.scripts/check_repository.pypasses.This resolves the deferred item in the chapter guide (§31.8). The only
remaining informal item in Chapter 31 is the POLLARD-RHO birthday-paradox
heuristic (documented as informal in CLRS).
🤖 Generated with Claude Code