feat(ch34): NP-Completeness theorem layer complete (composition, P⊆NP, ≤_P transitivity, complement, union, intersection)

[TankTechnology]

Green-field Chapter 34 (NP-Completeness) on Mathlib's
Turing.TM2ComputableInPolyTime (machine-level polynomial-time computability
with Polynomial ℕ time bounds). The theorem layer of Sections 34.1–34.3 is
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's
  proof_wanted TM2ComputableInPolyTime.comp via the shared-stack two-phase
  TM2 machine Turing.TM2Comp.compMachine (Composition.lean).
• PolyTimeDecidable.compl / ClassP_compl — P closed under complement
  (via the Bool.not machine Turing.TM2Comp.notMachine).
• PolyTimeDecidable.union / ClassP_union and PolyTimeDecidable.inter /
  ClassP_inter — P closed under union and intersection, via the AND/OR
  machine Turing.TM2AndOr.andOrMachine (AndOr.lean): a four-phase TM2 that
  duplicates the input onto both deciders' stacks, runs M₁ then M₂
  sequentially, and combines the two Bool results with AND/OR.

Section 34.2 — Polynomial-Time Verification

• PolyTimeVerifiable / ClassNP / mem_ClassNP.
• PolyTimeVerifiable.of_decidable and ClassP_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 ≤_P via the composition
  closure.

Remaining chapter scope (documented, not sorry)

• Sections 34.4–34.5 specific reductions (CIRCUIT-SAT, SAT, 3-CNF-SAT,
  CLIQUE, VERTEX-COVER, HAM-CYCLE, SUBSET-SUM) are not yet represented.
• The empty/universal languages in P as concrete machine constructions.
• Open problems (P vs NP) are intentionally out of scope.

Verification

• lake build CLRSLean passes (no sorry/admit; the headline theorems
  depend only on propext/Classical.choice/Quot.sound).
• check_repository.py and check_progress_csv.py --write-dashboard pass.
• literate.toml / edition map / progress CSV / Progress.lean / README /
  index / proof-map / progress-CSV tests synced.

🤖 Generated with Claude Code