@[reducible, inline]

abbrev PCP.BinaryString (n : ℕ) : Type

def PCP.Language : Type

def PCP.IsPolynomial (f : ℕ → ℕ) : Prop

structure PCP.NPVerifier (n witnessLen : ℕ) : Type

• decide : BinaryString n → BinaryString witnessLen → Bool

def PCP.InNP (L : Language) : Prop

structure PCP.PCPVerifier (n : ℕ) : Type

• numRandom : ℕ
• numQueries : ℕ
• proofLen : ℕ
• queryPositions : BinaryString self.numRandom → Fin self.numQueries → Fin self.proofLen
• decide : BinaryString n → BinaryString self.numRandom → BinaryString self.numQueries → Bool

def PCP.PCPVerifier.accepts {n : ℕ} (V : PCPVerifier n) (x : BinaryString n) (π : BinaryString V.proofLen) (r : BinaryString V.numRandom) : Bool

def PCP.PCPVerifier.hasCompleteness {n : ℕ} (V : PCPVerifier n) (L : Language) : Prop

def PCP.PCPVerifier.hasSoundness {n : ℕ} (V : PCPVerifier n) (L : Language) (s : ℝ) : Prop

def PCP.IsOLogN (f : ℕ → ℕ) : Prop

def PCP.IsO1 (f : ℕ → ℕ) : Prop

def PCP.InPCP (L : Language) (rBound qBound : (ℕ → ℕ) → Prop) : Prop

structure PCP.Literal (n : ℕ) : Type

• var : Fin n
• polarity : Bool

structure PCP.Clause (n : ℕ) : Type

• lit₁ : Literal n
• lit₂ : Literal n
• lit₃ : Literal n

@[reducible, inline]

abbrev PCP.Assignment (n : ℕ) : Type

def PCP.Literal.satisfiedBy {n : ℕ} (l : Literal n) (σ : Assignment n) : Bool

def PCP.Clause.satisfiedBy {n : ℕ} (c : Clause n) (σ : Assignment n) : Bool

structure PCP.ThreeSATFormula : Type

• numVars : ℕ
• clauses : List (Clause self.numVars)
• clauses_nonempty : self.clauses ≠ []

def PCP.numSatisfied (φ : ThreeSATFormula) (σ : Assignment φ.numVars) : ℕ

def PCP.IsSatisfiable (φ : ThreeSATFormula) : Prop

def PCP.HasMaxSatFractionAtMost (φ : ThreeSATFormula) (s : ℝ) : Prop

opaque PCP.IsPolyTimeReduction : ((n : ℕ) → BinaryString n → ThreeSATFormula) → Prop

def PCP.Gap3SAT_IsNPHard (s : ℝ) : Prop

theorem PCP.pcp_theorem_gap3SAT : ∃ (s : ℝ), 0 < s ∧ s < 1 ∧ Gap3SAT_IsNPHard s