GapCVP proof, part 18

structure GapCVP.Comparator.PromiseProblem : Type

The disjoint yes and no languages used by the canonical hardness statements.

• yes : BitLanguage

  Encodings satisfying the promise's positive case.

• no : BitLanguage

  Encodings satisfying the promise's negative case.

• disjoint (bits : List Bool) : self.yes bits = true → self.no bits = true → False

noncomputable def GapCVP.Comparator.gapCVP400Promise : PromiseProblem

GapCVP reduction support.

Equations

• GapCVP.Comparator.gapCVP400Promise = { yes := GapCVP.Comparator.yesLanguage✝, no := GapCVP.Comparator.noLanguage✝, disjoint := GapCVP.Comparator.gapCVP400Promise._proof_1 }

noncomputable def GapCVP.Comparator.binaryNearestCodewordPromise : PromiseProblem

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.Comparator.binarySyndromeDecodingPromise : PromiseProblem

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.Comparator.finitePGapCVPPromise (p : ℚ) (hp : 1 ≤ p) : PromiseProblem

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

structure GapCVP.Comparator.PromiseReduction (language : BitLanguage) (problem : PromiseProblem) : Type

A polynomial-time reduction sending members to yes-instances and nonmembers to no-instances.

• map : List Bool → List Bool

  The transformation of encoded instances.

• polynomial_time : Nonempty (BitTM self.map)
• completeness (input : List Bool) : language input = true → problem.yes (self.map input) = true
• soundness (input : List Bool) : ¬language input = true → problem.no (self.map input) = true

noncomputable def GapCVP.Comparator.IsNPHardPromise (problem : PromiseProblem) : Bool

GapCVP reduction support.

Equations

• GapCVP.Comparator.IsNPHardPromise problem = decide (∀ (language : GapCVP.BitLanguage), GapCVP.IsNP language = true → Nonempty (GapCVP.Comparator.PromiseReduction language problem))

theorem GapCVP.Comparator.gapCVP400IsNPHard : IsNPHardPromise gapCVP400Promise = true

theorem GapCVP.Comparator.binaryNearestCodewordIsNPHard : IsNPHardPromise binaryNearestCodewordPromise = true

theorem GapCVP.Comparator.binarySyndromeDecodingIsNPHard : IsNPHardPromise binarySyndromeDecodingPromise = true

theorem GapCVP.Comparator.finitePNormGapCVPIsNPHard (p : ℚ) (hp : 1 ≤ p) : IsNPHardPromise (finitePGapCVPPromise p hp) = true