Executable six-query assignment testing

The selected tester reuses the executable coefficient table and the shared five-check family. Its coin string retains the original product coins together with a branch in Fin 5. Only the selected branch's six padded queries are read. All supplied data are charged by the certificates; as in Encoded.AssignmentTester, polynomial time is for each fixed alphabet, not uniformly in the alphabet size.

Main definitions

• Cslib.PCP.Encoded.SelectedHadamardTester.localTest: the executable selected tester.
• Cslib.PCP.Encoded.SelectedHadamardTester.query, .accepts: query and decision algorithms.

Main results

• Cslib.PCP.Encoded.SelectedHadamardTester.localTest_eq: exact interpretation.
• Cslib.PCP.Encoded.SelectedHadamardTester.isPolyTime_query, .isPolyTime_accepts: efficiency certificates uniform in the supplied constraint, coins, and answers.

References

• I. Dinur, The PCP theorem by gap amplification

def Cslib.PCP.Encoded.SelectedHadamardTester.localTest {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) : LocalTest (HadamardTester.Pos α) (Fin 5 × HadamardTester.Rand α) (Fin 6) Bool

Select a check using executable quadratic coefficients.

theorem Cslib.PCP.Encoded.SelectedHadamardTester.localTest_eq {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) : localTest constraint = selectedHadamardTester fun (a b : α) => constraint a b = true

The executable selected tester agrees exactly with the mathematical one.

def Cslib.PCP.Encoded.SelectedHadamardTester.query {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : Fin 5 × HadamardTester.Rand α) (i : Fin 6) : HadamardTester.Pos α

Compute one of the six queries for the specified branch and product coins.

def Cslib.PCP.Encoded.SelectedHadamardTester.accepts {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : Fin 5 × HadamardTester.Rand α) (answers : Fin 6 → Bool) : Bool

Decide the selected check, ignoring padding answers.

theorem Cslib.PCP.Encoded.SelectedHadamardTester.query_eq {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : Fin 5 × HadamardTester.Rand α) (i : Fin 6) : query constraint coins i = (selectedHadamardTester fun (a b : α) => constraint a b = true).query coins i

Computed queries agree with the selected mathematical tester.

@[simp]

theorem Cslib.PCP.Encoded.SelectedHadamardTester.accepts_eq_true {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : Fin 5 × HadamardTester.Rand α) (answers : Fin 6 → Bool) : accepts constraint coins answers = true ↔ (selectedHadamardTester fun (a b : α) => constraint a b = true).Accepts coins answers

The executable decision expresses exactly the selected acceptance predicate.

theorem Cslib.PCP.Encoded.SelectedHadamardTester.isPolyTime_query {α : Type} [Fintype α] [DecidableEq α] (coinsEncoding : Fin 5 × HadamardTester.Rand α ↪ List Bool) (queryEncoding : Fin 6 ↪ List Bool) (positionEncoding : HadamardTester.Pos α ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (α → α → Bool) × (Fin 5 × HadamardTester.Rand α) × Fin 6) => query p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair coinsEncoding queryEncoding)) positionEncoding

Query generation charges the runtime constraint, selected branch, and product coins.

theorem Cslib.PCP.Encoded.SelectedHadamardTester.isPolyTime_accepts {α : Type} [Fintype α] [DecidableEq α] (coinsEncoding : Fin 5 × HadamardTester.Rand α ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (α → α → Bool) × (Fin 5 × HadamardTester.Rand α) × (Fin 6 → Bool)) => accepts p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair coinsEncoding (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool

Acceptance charges the full supplied input, including all six answers.