Håstad's clique inapproximability theorem
Lax253009.CliqueHardness · concepts/Lax253009/CliqueHardness.lean · lax-253009
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For every fixed real , a deterministic polynomial-time -approximation of the clique number would imply . Equivalently, if , no such approximation exists. This is Theorem 5.2 of Håstad's paper.
The approximation convention includes a single uniform algorithm and all nonempty finite graphs. NP is the binary-language class from lax-434930; ZPP is the bounded-time, failure-allowed class from lax-666725. No complexity class is redefined here. The proof implements the reductions in these machine models, with an explicit polynomial clock and exact preservation of the finite fair-coin output distribution.
Concept map
Evidence
This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.
1 approximation_implies_np_eq_zpp proven
-
- thm✓
Lax253009.Amplification - thm✓
Lax253009.CenteredProjection - thm✓
Lax253009.EncodedReduction - thm✓
Lax253009.FAFComposition - thm✓
Lax253009.FAFLocalTests - thm✓
Lax253009.FAFPatterns - thm✓
Lax253009.FiniteProbability - thm✓
Lax253009.FreshBitSampling - thm✓
Lax253009.GraphEncoding - thm✓
Lax253009.ProjectionEncoding - lem✓
Lax253009.RandomizedContainments - thm✓
Lax253009.RandomizedReduction - thm✓
Lax253009.SamplingParameters - thm✓
Lax253009.TestRepetition - thm✓
Lax253009.TestSampling
- thm✓
2 not_approximable proven
Lean source view on GitHub
| 1 | import Lax253009.Approximation |
| 2 | import Lax434930.NondeterministicPolynomialTime |
| 3 | import Lax666725.ZeroError |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Håstad's clique inapproximability theorem |
| 8 | type: theorem |
| 9 | --- |
| 10 | For every fixed real , a deterministic polynomial-time |
| 11 | -approximation of the clique number would imply |
| 12 | . Equivalently, if , |
| 13 | no such approximation exists. This is Theorem 5.2 of Håstad's paper. |
| 14 | |
| 15 | The approximation convention includes a single uniform algorithm and all |
| 16 | nonempty finite graphs. NP is the binary-language class from lax-434930; |
| 17 | ZPP is the bounded-time, failure-allowed class from lax-666725. No complexity |
| 18 | class is redefined here. The proof implements the reductions in these machine |
| 19 | models, with an explicit polynomial clock and exact preservation of the |
| 20 | finite fair-coin output distribution. |
| 21 | -/ |
| 22 | |
| 23 | namespace Lax253009.CliqueHardness |
| 24 | |
| 25 | open Approximation |
| 26 | open Lax434930.NondeterministicPolynomialTime Lax666725.ZeroError |
| 27 | |
| 28 | axiom approximation_implies_np_eq_zpp (ε : ℝ) (hε : 0 < ε) : |
| 29 | Approximable ε → NP = ZPP |
| 30 | |
| 31 | axiom not_approximable (ε : ℝ) (hε : 0 < ε) (hne : NP ≠ ZPP) : |
| 32 | ¬ Approximable ε |
| 33 | |
| 34 | end Lax253009.CliqueHardness |
| 35 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments