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
@[reducible, inline]
abbrev Cslib.PCP.SelectedAlphabet :
Type

The fixed 128-symbol answer alphabet Bool × (Fin 6 → Bool) of composition with the selected six-query Hadamard assignment tester: one proof bit and six claimed query answers.

Instances For
    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) SelectedAlphabet

      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 SelectedAlphabet = 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.