Composition with a binary-constraint assignment tester

An AssignmentTester reads two encoded input labels and an auxiliary proof. Its construction is separate from perfect completeness and soundness relative to a supplied decoder. The latter asks only that a violated decoded constraint causes rejection with probability at least δ; it is not the stronger distance-soundness contract of an assignment tester for arbitrary circuits.

Composition shares each vertex's input table between all incident testers and gives each edge its own auxiliary table. The existing local-test graph construction then loses a factor |Q| / δ in value, independently of the particular encoding, decoder, and tester. No executable construction or efficiency assertion is included in this mathematical interface.

Main definitions

• Cslib.PCP.AssignmentTester: a tester, an input encoding, and honest auxiliary proofs.
• Cslib.PCP.AssignmentTester.IsComplete, Cslib.PCP.AssignmentTester.Sound: its certificates.
• Cslib.PCP.AssignmentTester.compose: the composed constraint graph.

Main results

• Cslib.PCP.AssignmentTester.unsatVal_compose_le: quantitative perfect completeness.
• Cslib.PCP.AssignmentTester.mul_unsatFrac_decodeLabelling_le: weighted soundness.
• Cslib.PCP.AssignmentTester.le_unsatVal_compose: composition loses at most |Q| / δ.
• Cslib.PCP.AssignmentTester.satisfiable_compose_iff: preservation of satisfiability.

References

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

def Cslib.PCP.ConstraintGraph.ends {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) (e : E) : Fin 2 → V

The two ends of an edge: the first one at 0, the second one at 1.

@[simp]

theorem Cslib.PCP.ConstraintGraph.ends_zero {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) (e : E) : G.ends e 0 = G.src e

@[simp]

theorem Cslib.PCP.ConstraintGraph.ends_one {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) (e : E) : G.ends e 1 = G.dst e

structure Cslib.PCP.AssignmentTester (α : Type u_1) (I : Type u_2) (P : Type u_3) (R : Type u_4) (Q : Type u_5) (Γ : Type u_6) : Type (max (max (max (max (max u_1 u_2) u_3) u_4) u_5) u_6)

Data for testing binary constraints on α, with input positions I, auxiliary positions P, coins R, queries Q, and proof symbols Γ. Correctness is supplied separately.

• test : (α → α → Prop) → LocalTest (Fin 2 × I ⊕ P) R Q Γ

  The local test for a binary constraint.

• encode : α → I → Γ

  The input table of a label.

• auxiliary : (α → α → Prop) → (Fin 2 → α) → P → Γ

  The honest auxiliary table for a constraint and two input labels.

def Cslib.PCP.AssignmentTester.honestProof {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} (T : AssignmentTester α I P R Q Γ) (C : α → α → Prop) (σ : Fin 2 → α) : Fin 2 × I ⊕ P → Γ

The two honest input tables together with the honest auxiliary table.

def Cslib.PCP.AssignmentTester.IsComplete {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} (T : AssignmentTester α I P R Q Γ) : Prop

Every satisfied constraint accepts its honest proof for every random string.

def Cslib.PCP.AssignmentTester.Sound {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} (T : AssignmentTester α I P R Q Γ) [Fintype R] (decode : (I → Γ) → α) (δ : ℝ) : Prop

A constraint violated by the decoded input tables is rejected with probability at least δ. The decoder need not be computable; it is used only in the soundness argument.

@[reducible, inline]

abbrev Cslib.PCP.AssignmentTester.ComposePos (V : Type u_9) (E : Type u_10) (I : Type u_11) (P : Type u_12) : Type (max (max u_11 u_9) u_12 u_10)

Shared vertex input tables and separate edge auxiliary tables.

def Cslib.PCP.AssignmentTester.testerPos {α : Type u_1} {I : Type u_2} {P : Type u_3} {V : Type u_7} {E : Type u_8} (G : ConstraintGraph V E α) (e : E) : Fin 2 × I ⊕ P → ComposePos V E I P

The part of a composed proof read by the tester of an edge.

def Cslib.PCP.AssignmentTester.composeTest {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} (T : AssignmentTester α I P R Q Γ) (G : ConstraintGraph V E α) : LocalTest (ComposePos V E I P) (E × R) Q Γ

Run the tester of a uniformly random edge on its input and auxiliary tables.

def Cslib.PCP.AssignmentTester.compose {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} (T : AssignmentTester α I P R Q Γ) (G : ConstraintGraph V E α) : ConstraintGraph (ComposePos V E I P ⊕ E × R) ((E × R) × Q) (Γ × (Q → Γ))

The constraint graph of the composed local test.

def Cslib.PCP.AssignmentTester.composeProof {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} (T : AssignmentTester α I P R Q Γ) (G : ConstraintGraph V E α) (σ : V → α) : ComposePos V E I P → Γ

Encode every vertex label and fill every edge's auxiliary table honestly.

theorem Cslib.PCP.AssignmentTester.composeProof_comp_testerPos {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} (T : AssignmentTester α I P R Q Γ) (G : ConstraintGraph V E α) (σ : V → α) (e : E) : T.composeProof G σ ∘ testerPos G e = T.honestProof (G.rel e) fun (b : Fin 2) => σ (G.ends e b)

A local tester reads the honest proof of its endpoint labels.

theorem Cslib.PCP.AssignmentTester.passes_composeTest_composeProof {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} {T : AssignmentTester α I P R Q Γ} (hcomplete : T.IsComplete) (G : ConstraintGraph V E α) {σ : V → α} {e : E} (he : G.Satisfies σ e) (r : R) : (T.composeTest G).Passes (T.composeProof G σ) (e, r)

A satisfied edge's tester accepts the honest composed proof.

theorem Cslib.PCP.AssignmentTester.satisfiable_compose {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} {T : AssignmentTester α I P R Q Γ} [Nonempty Γ] (hcomplete : T.IsComplete) {G : ConstraintGraph V E α} (h : G.Satisfiable) : (T.compose G).Satisfiable

Perfect completeness of composition.

theorem Cslib.PCP.AssignmentTester.unsatFrac_compose_labellingOf_le {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} {T : AssignmentTester α I P R Q Γ} [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Q] [Fintype E] (hcomplete : T.IsComplete) (G : ConstraintGraph V E α) (σ : V → α) (γ : Γ) : (T.compose G).unsatFrac ((T.composeTest G).labellingOf (T.composeProof G σ) γ) ≤ G.unsatFrac σ

Honest composition violates no greater fraction of edges than the original labelling.

theorem Cslib.PCP.AssignmentTester.unsatVal_compose_le {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} {T : AssignmentTester α I P R Q Γ} [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Q] [Fintype E] [Nonempty α] [Nonempty Γ] (hcomplete : T.IsComplete) (G : ConstraintGraph V E α) : (T.compose G).unsatVal ≤ G.unsatVal

Quantitative perfect completeness: composition does not increase the value.

def Cslib.PCP.AssignmentTester.decodeLabelling {α : Type u_1} {I : Type u_2} {P : Type u_3} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} (decode : (I → Γ) → α) (π : ComposePos V E I P → Γ) (v : V) : α

Decode the shared input table of each vertex.

theorem Cslib.PCP.AssignmentTester.mul_unsatFrac_decodeLabelling_le {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} {T : AssignmentTester α I P R Q Γ} [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Q] [Fintype E] {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (G : ConstraintGraph V E α) (A : ComposePos V E I P ⊕ E × R → Γ × (Q → Γ)) : δ * G.unsatFrac (decodeLabelling decode (LocalTest.proofOf A)) ≤ ↑(Fintype.card Q) * (T.compose G).unsatFrac A

Weighted soundness: every violated decoded edge contributes δ rejection probability, and each rejecting local test contributes at least one of its |Q| edges.

theorem Cslib.PCP.AssignmentTester.le_unsatVal_compose {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} {T : AssignmentTester α I P R Q Γ} [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Q] [Fintype E] [Nonempty Γ] {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (hδ : 0 < δ) (G : ConstraintGraph V E α) : G.unsatVal / (↑(Fintype.card Q) / δ) ≤ (T.compose G).unsatVal

Soundness of composition: the value decreases by at most the factor |Q| / δ.

theorem Cslib.PCP.AssignmentTester.satisfiable_compose_iff {α : Type u_1} {I : Type u_2} {P : Type u_3} {R : Type u_4} {Q : Type u_5} {Γ : Type u_6} {V : Type u_7} {E : Type u_8} {T : AssignmentTester α I P R Q Γ} [Fintype R] [Nonempty R] [Nonempty Q] [Finite E] [Finite Q] [Nonempty α] [Nonempty Γ] (hcomplete : T.IsComplete) {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (hδ : 0 < δ) (G : ConstraintGraph V E α) : (T.compose G).Satisfiable ↔ G.Satisfiable

A positive rejection bound and perfect completeness preserve satisfiability.