Selecting one check of the Hadamard assignment tester

The five checks of hadamardTester make at most six queries each. Selecting one uniformly, instead of running their conjunction, reduces the query count from seventeen to six. The union bound loses at most a factor of five in rejection. The original product of random strings is retained, so this construction makes no claim of saving random bits.

Main definitions

• Cslib.PCP.HadamardTester.checks: the five checks, padded to a common six-query interface.
• Cslib.PCP.selectedHadamardTester: the tester selecting one of those checks uniformly.

Main results

• Cslib.PCP.HadamardTester.one_sub_acceptProb_le_five_mul_selected: rejection comparison.
• Cslib.PCP.HadamardTester.passes_selected_honestProof: perfect completeness.
• Cslib.PCP.HadamardTester.exists_inputDist_div_le_one_sub_acceptProb_selected: proximity soundness with loss 140.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• I. Dinur, The PCP theorem by gap amplification

def Cslib.PCP.HadamardTester.checks {α : Type u_1} [Fintype α] (coeff : (Fin 2 × α) × Fin 2 × α ⊕ Fin 2 → (Fin 2 × α) × Fin 2 × α → Bool) : Fin 5 → LocalTest (Pos α) (Rand α) (Fin 6) Bool

The five checks on a common coin space and six query positions. The coefficient table is an argument so that the same construction works with mathematical and executable constraints.

noncomputable def Cslib.PCP.selectedHadamardTester {α : Type u_1} [Fintype α] [DecidableEq α] (C : α → α → Prop) : LocalTest (HadamardTester.Pos α) (Fin 5 × HadamardTester.Rand α) (Fin 6) Bool

Select one of the five Hadamard checks uniformly. Shorter checks repeat queries to reach six positions; their acceptance predicates ignore the extra answers.

theorem Cslib.PCP.HadamardTester.one_sub_acceptProb_le_five_mul_selected {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} (π : Pos α → Bool) : 1 - (hadamardTester C).acceptProb π ≤ 5 * (1 - (selectedHadamardTester C).acceptProb π)

Selecting a single check loses at most a factor of five in rejection probability.

theorem Cslib.PCP.HadamardTester.passes_selected_honestProof {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {σ : Fin 2 → α} (hσ : C (σ 0) (σ 1)) (ω : Fin 5 × Rand α) : (selectedHadamardTester C).Passes (honestProof σ) ω

Every selected check passes the honest proof of satisfying labels.

theorem Cslib.PCP.HadamardTester.acceptProb_selected_honestProof {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {σ : Fin 2 → α} (hσ : C (σ 0) (σ 1)) : (selectedHadamardTester C).acceptProb (honestProof σ) = 1

Perfect completeness of the six-query tester.

theorem Cslib.PCP.HadamardTester.exists_inputDist_le_of_le_acceptProb_selected {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} {π : Pos α → Bool} {ρ : ℝ} (hρ : ρ < 1 / 140) (h : 1 - ρ ≤ (selectedHadamardTester C).acceptProb π) : ∃ (σ : Fin 2 → α), C (σ 0) (σ 1) ∧ inputDist π σ ≤ 15 * ρ

High acceptance by the selected tester decodes to satisfying labels near the input tables.

theorem Cslib.PCP.HadamardTester.exists_inputDist_div_le_one_sub_acceptProb_selected {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} (hC : ∃ (a : α) (b : α), C a b) (π : Pos α → Bool) : ∃ (σ : Fin 2 → α), C (σ 0) (σ 1) ∧ inputDist π σ / 140 ≤ 1 - (selectedHadamardTester C).acceptProb π

Proximity soundness of the six-query tester, with rejection coefficient 1/140.

theorem Cslib.PCP.HadamardTester.one_div_le_one_sub_acceptProb_selected_of_forall_not {α : Type u_1} [Fintype α] [DecidableEq α] {C : α → α → Prop} (hC : ∀ (a b : α), ¬C a b) (π : Pos α → Bool) : 1 / 140 ≤ 1 - (selectedHadamardTester C).acceptProb π

An unsatisfiable constraint is rejected with probability at least 1/140.