feat(ch34): NP-Completeness — theorem layer complete (composition, P⊆NP, ≤_P transitivity, complement, union, intersection) - #156
Closed
TankTechnology wants to merge 36 commits into
Closed
feat(ch34): NP-Completeness — theorem layer complete (composition, P⊆NP, ≤_P transitivity, complement, union, intersection)#156TankTechnology wants to merge 36 commits into
TankTechnology wants to merge 36 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>
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>
Green-field start of Chapter 34 on Mathlib's Turing.TM2ComputableInPolyTime (machine-level polynomial-time computability with Polynomial ℕ bounds). Section 34.1 defines the framework: - Language: a set of strings over an alphabet. - PolyTimeComputable: a function computed by a TM2 machine in polynomial time. - PolyTimeDecidable / ClassP: the class of polynomial-time decidable languages; mem_ClassP (kernel-clean, only propext/Quot.sound). Wiring: Chapter_34.lean guide, literate.toml, CLRSLean.lean import, FourthEdition guide now imports the source (status partial), interface test, edition-map (34.1 native), progress CSV (34 partial 1/1), proof map. Deferred (documented in the guide, not sorry): concrete machine constructions (empty/universal in P), Turing.TM2ComputableInPolyTime.comp (Mathlib proof_wanted), ClassP closure, then 34.2 NP and 34.3 reducibility. Open problems (P vs NP) and specific reductions (34.4-34.5) are out of scope per the session plan. Verification: lake build CLRSLean passes; check_repository.py passes; test_check_progress_csv.py updated (1,328 -> 1,329; not-started 5 -> 4). Co-Authored-By: Claude <noreply@anthropic.com>
Extends the green-field NP-completeness formalization with the rest of the conceptual framework: - 34.2 Polynomial-Time Verification: pairEncoding (certificate/input encoding with a separator), PolyTimeVerifiable, ClassNP, mem_ClassNP. - 34.3 NP-Completeness and Reducibility: PolyTimeReducible (L₁ ≤_P L₂), NPHard, NPComplete, ClassNPC. Wiring: chapter guide lists all three sections; literate.toml, index.md, edition map (34.2, 34.3 native), progress CSV (34 partial 3/3, 34.1-34.3 represented), interface test, README/progress dashboard regenerated. The theorem layer remains the documented next milestone: Turing.TM2ComputableInPolyTime.comp (polytime-composition closure; Mathlib leaves this proof_wanted — a combined-machine construction is partially developed), P ⊆ NP, transitivity of PolyTimeReducible, and the NP-completeness characterization. Open problems (P vs NP) and the specific reductions (34.4-34.5) remain out of scope. Verification: lake build CLRSLean passes; check_repository.py passes; tests updated (1,329 -> 1,331). Co-Authored-By: Claude <noreply@anthropic.com>
Shared-stack composition construction for `TM2ComputableInPolyTime.comp` (scratch): the combined machine has stacks `Sum K₁ K₂`; phase 1 runs `h1`'s program reindexed `k ↦ inl k` (`halt` jumps into `h2`'s main); phase 2 runs `h2`'s program with its input stack implemented by `h1`'s output stack (`convIn`/`convOut` through the alphabet equivalence). `stepAux_mapStmt₁`/`stepAux_mapStmt₂` and `step₁_sim`/`step₂_sim` show every combined step mirrors the underlying machine's step. Co-Authored-By: Claude <noreply@anthropic.com>
`evalsTo_lift`/`evalsToInTime_lift` transport an evaluation through a step simulation; `stepAux_stk_len_pushCount` + `maxPushCount₁` bound any stack's growth per step, giving `evalsTo_out_len_le` (output length ≤ input length + linear in steps) — the input to phase 2's time bound. `compTime` combines `h1.time` with `h2.time.comp (X + h1.time)`. Co-Authored-By: Claude <noreply@anthropic.com>
`mapCfg₁_init`, `mapCfg₁_halt_eq`, and `mapCfg₂_halt_eq` connect the embedded configurations. The final piece, `mapCfg₂_halt_eq`, needed the composite `compOutputAlphabet` — an `Equiv.cast` recast when `h2` reuses its input stack as output — to reduce element-wise. Making `compMachine` an `abbrev` (reducible) lets `rw` see `(compMachine h1 h2).Γ (compMachine h1 h2).k₁` as `CompΓ h1 h2 (compk₁ h1 h2)`; the `⋯ ▸` cast round-trip closes via the new `cast_symm_cancel` (proof irrelevance). Axiom-clean (`propext`/ `Classical.choice`/`Quot.sound` only). Co-Authored-By: Claude <noreply@anthropic.com>
Closes Mathlib's `proof_wanted TM2ComputableInPolyTime.comp`. `comp_outputsFun` runs the combined machine in two phases: phase 1 lifted through `mapCfg₁`, meeting `mapCfg₁_halt_eq`, phase 2 through `mapCfg₂`, closing with `mapCfg₂_halt_eq`, chained by `EvalsToInTime.trans`. The total time `m₂ + m₁` is bounded by `compTime` using the new `Polynomial.eval_mono_nat` (`eval` on `Polynomial ℕ` is monotone — nonnegative coefficients at a nonnegative argument) and the phase-1 output-length bound `evalsTo_out_len_le`. `comp_scratch` proves `Nonempty (TM2ComputableInPolyTime eα eγ (g ∘ f))`, axiom-clean (`propext`/`Classical.choice`/`Quot.sound` only). Co-Authored-By: Claude <noreply@anthropic.com>
…o 34.3 Move the composition construction from the scratch into `Section_34_1_Polynomial_Time/Composition.lean` (module `...Composition`, namespace `Turing.TM2Comp`): the combined two-phase machine, step simulations, configuration bridges, time bound, and `comp_scratch` (Mathlib's `proof_wanted TM2ComputableInPolyTime.comp`). Section 34.1 now proves `PolyTimeComputable.comp` (composition closure, CLRS §34.1); section 34.3 proves `PolyTimeReducible.trans` (transitivity of `≤_P`, CLRS §34.3). The root `Scratch_comp.lean` is removed. Co-Authored-By: Claude <noreply@anthropic.com>
`Section_34_2_Polynomial_Time_Verification/PairProjection.lean` builds the pair-projection machine `prjMachine` (three stacks, phases scan/copy₁/copy₂/fin; the LIFO double pass through `temp` outputs `y` in order) and proves `prjComputableInPolyTime` (`pairEncoding x y ↦ y` is polytime). The phase lemmas (`scan_phase`, `copy1_phase`, `copy2_phase`, `fin_step`) run the machine's `(flip bind Sstep)^[n]` iteration. Section 34.2 proves `PolyTimeVerifiable.of_decidable` (a decider is a verifier that ignores the certificate, composed with the projection machine) and `ClassP_subset_ClassNP` (`P ⊆ NP`, CLRS Theorem 34.2). `pairEncoding` moves from 34.2 to 34.1 so both 34.2 and the projection module can import it without a cycle. Axiom-clean. Co-Authored-By: Claude <noreply@anthropic.com>
`Turing.TM2Comp.boolEncoding`/`notMachine`/`notComputableInPolyTime` (in the Composition module) compute `Bool.not` on the one-symbol encoding in one step. Section 34.1 proves `PolyTimeDecidable.compl` (negate the decider, composed with the NOT machine) and `ClassP_compl` (closure of `P` under complement, CLRS §34.1). `boolEncoding` becomes an alias to the shared `Turing.TM2Comp` def. Co-Authored-By: Claude <noreply@anthropic.com>
Chapter 34's theorem layer (polytime composition, P ⊆ NP, transitivity of `≤_P`, P closed under complement) is complete. Sync the ledger and site configuration: - `docs/clrs-proof-progress.csv`: 6 tracked / 6 proved; theorem-layer note; remaining gap = Sections 34.4-34.5 + P closed under union/intersection. - Regenerated `CLRSLean/Progress.lean` and the README progress table (total 1334 theorem entries; `test_check_progress_csv.py` count updated). - `literate.toml`: register the `Composition` and `PairProjection` modules. - `docs/index.md`, `docs/proof-map.md`, `CLRSLean/Chapter_34.lean` (aggregator imports the sub-modules), and the fourth-edition guide: coverage boundary updated. Co-Authored-By: Claude <noreply@anthropic.com>
Closes the last theorem-layer gap of Chapter 34: P is closed under union and intersection. The construction is Turing.TM2AndOr, a four-phase TM2 machine that duplicates the input onto both deciders' input stacks (dupScan/dupRestore via a scratch stack), runs M₁ then M₂ sequentially on their own stack halves, and combines the two Bool results with AND/OR. - Section_34_1_Polynomial_Time/AndOr.lean (856 lines, kernel-clean): andOrMachine, mapStmt₁/mapStmt₂ reindexings, dup phase lemmas (dup_copyout_phase/dup_restore_phase/dup_phase), combine_step, mapCfg₁to₂ bridge, andOrTime, andOr_outputsFun, and andOrComputableInPolyTime (x ↦ [op (f₁ x) (f₂ x)] polytime). - Section_34_1: PolyTimeDecidable.union/inter and ClassP_union/inter. - Docs/literate.toml/index/README/proof-map/progress CSV synced; repo checker passes; headline theorems depend only on propext/Classical.choice/Quot.sound. Co-Authored-By: Claude <noreply@anthropic.com>
TankTechnology
changed the title
Owner
Author
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.
Green-field Chapter 34 (NP-Completeness), building on Mathlib's
Turing.TM2ComputableInPolyTime(machine-level polynomial-time computabilitywith
Polynomial ℕtime bounds). The theorem layer of Sections 34.1–34.3 isnow complete and kernel-clean.
Section 34.1 — Polynomial Time (framework + closure properties)
CLRS.Chapter34.Language/PolyTimeComputable/PolyTimeDecidable/ClassP/mem_ClassP.PolyTimeComputable.comp— polytime composition closure, closing Mathlib'sproof_wanted TM2ComputableInPolyTime.compvia the shared-stack two-phaseTM2 machine
Turing.TM2Comp.compMachine(Composition.lean).PolyTimeDecidable.compl/ClassP_compl—Pclosed under complement(via the
Bool.notmachineTuring.TM2Comp.notMachine).PolyTimeDecidable.union/ClassP_unionandPolyTimeDecidable.inter/ClassP_inter—Pclosed under union and intersection, via the AND/ORmachine
Turing.TM2AndOr.andOrMachine(AndOr.lean): a four-phase TM2 thatduplicates the input onto both deciders' stacks, runs
M₁thenM₂sequentially, and combines the two
Boolresults with AND/OR.Section 34.2 — Polynomial-Time Verification
PolyTimeVerifiable/ClassNP/mem_ClassNP.PolyTimeVerifiable.of_decidableandClassP_subset_ClassNP—P ⊆ NP(Theorem 34.2), via the pair-projection machine
Turing.Prj.prjMachine(
PairProjection.lean).Section 34.3 — NP-Completeness and Reducibility
PolyTimeReducible/NPHard/NPComplete/ClassNPC.PolyTimeReducible.trans— transitivity of≤_Pvia the compositionclosure.
Remaining chapter scope (documented, not
sorry)CLIQUE, VERTEX-COVER, HAM-CYCLE, SUBSET-SUM) are not yet represented.
Pas concrete machine constructions.Verification
lake build CLRSLeanpasses (nosorry/admit; the headline theoremsdepend only on
propext/Classical.choice/Quot.sound).check_repository.pyandcheck_progress_csv.py --write-dashboardpass.🤖 Generated with Claude Code