Documentation

Complexity.Computability.PCP.SelectedComposition

Composition with the six-query assignment tester #

The selected Hadamard tester is a second instance of the generic binary-constraint composition interface. Its rejection coefficient is 1/140; six queries give a composition loss of 840. The composed alphabet has 128 symbols, compared with 2^18 for the conjunction tester.

These are local composition parameters. They do not assert a six-query bound for the final binary-proof verifier, which additionally encodes labels and repeats its test.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.PCP.HadamardTester.selectedAssignmentTester {α : Type u_1} [Fintype α] [DecidableEq α] :
AssignmentTester α (α → Bool) (LinPos α ⊕ QuadPos α) (Fin 5 × Rand α) (Fin 6) Bool

Use the same label encoding and honest auxiliary tables, selecting just one check.

Instances For
    source
    theorem Cslib.PCP.HadamardTester.isComplete_selectedAssignmentTester {α : Type u_1} [Fintype α] [DecidableEq α] :
    selectedAssignmentTester.IsComplete

    Every selected check accepts an honest proof of a satisfied constraint.

    source
    theorem Cslib.PCP.HadamardTester.sound_selectedAssignmentTester {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] :
    selectedAssignmentTester.Sound ConstraintGraph.decodeLabel (1 / 140)

    The selected tester rejects every violated decoded constraint with probability at least 1/140. The decoder is identical to the conjunction tester's decoder.

    source
    noncomputable def Cslib.PCP.ConstraintGraph.composeSelected {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] (G : ConstraintGraph V E α) :
    ConstraintGraph (ComposePos V E α ⊕ E × Fin 5 × HadamardTester.Rand α) ((E × Fin 5 × HadamardTester.Rand α) × Fin 6) (Bool × (Fin 6 → Bool))

    Compose with one randomly selected Hadamard check per local test.

    Instances For
      source
      theorem Cslib.PCP.ConstraintGraph.unsatVal_composeSelected_le {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] :
      G.composeSelected.unsatVal ≤ G.unsatVal

      Quantitative perfect completeness of selected composition.

      source
      theorem Cslib.PCP.ConstraintGraph.le_unsatVal_composeSelected {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] :
      G.unsatVal / 840 ≤ G.composeSelected.unsatVal

      Six queries and rejection 1/140 give composition loss 840.

      source
      theorem Cslib.PCP.ConstraintGraph.satisfiable_composeSelected_iff {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] (G : ConstraintGraph V E α) [Finite E] [Nonempty α] :
      G.composeSelected.Satisfiable ↔ G.Satisfiable

      Selected composition preserves satisfiability.

      source
      theorem Cslib.PCP.ConstraintGraph.card_alphabet_composeSelected :
      Fintype.card (Bool × (Fin 6 → Bool)) = 128

      The selected composition alphabet stores one symbol and six claimed answers.

      source
      theorem Cslib.PCP.ConstraintGraph.card_vertices_composeSelected {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] [Fintype V] [Fintype E] :
      Fintype.card (ComposePos V E α ⊕ E × Fin 5 × HadamardTester.Rand α) = 2 ^ Fintype.card α * Fintype.card V + (2 ^ (2 * Fintype.card α) + 2 ^ (4 * Fintype.card α ^ 2) + 5 * 2 ^ (20 * Fintype.card α ^ 2 + 15 * Fintype.card α + 3)) * Fintype.card E

      The auxiliary tables are shared across the five checks; only the coin vertices are repeated.

      source
      theorem Cslib.PCP.ConstraintGraph.card_edges_composeSelected {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] [Fintype E] :
      Fintype.card ((E × Fin 5 × HadamardTester.Rand α) × Fin 6) = 30 * 2 ^ (20 * Fintype.card α ^ 2 + 15 * Fintype.card α + 3) * Fintype.card E

      Each original edge contributes five choices of check, the original coins, and six queries.