Proof of `Promise-gap hardness of Max Independent Set`
groundedproofs/Lax47Proofs/IndependentSetGapHardness.lean · lax-47
What this proof establishes
- 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.MajorityAmplification - thm✓
Lax253009.ProjectionEncoding - thm✓
Lax253009.RandomizedReduction - thm✓
Lax253009.SamplingParameters - thm✓
Lax253009.TestRepetition - thm✓
Lax253009.TestSampling
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Apply the registered PCP-to-clique gap reduction with exponent . The threshold guard converts its relative gap into the absolute independent-set gap on the complement. Graphs below the solver cutoff are handled by bounded exhaustive search. The finite-Turing adapter certifies this comparison, and independent majority trials provide the error bound needed for composition.