Documentation

Complexity.Computability.PCP.Encoded.SelectedComposition

Executable composition with the selected assignment tester #

The six-query tester supplies an executable realization to the shared graph compiler. Slot numbering, edge enumeration, interpretation, and resource accounting use the same implementation as conjunction composition. Complete coin and query lists recover mathematical selected composition; incomplete lists still give a well-formed graph when the input is well formed.

Main definitions #

Main results #

References #

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

The selected tester's query and acceptance algorithms, independent of its specification.

Instances For
    source
    theorem Cslib.PCP.Encoded.SelectedHadamardTester.realizes_implementation {α : Type} [Fintype α] [DecidableEq α] :
    implementation.Realizes HadamardTester.selectedAssignmentTester

    The executable algorithms realize the mathematical selected tester.

    source
    @[reducible, inline]
    abbrev Cslib.PCP.Encoded.Graph.SelectedComposeSlot (α : Type) :
    Type

    Input, auxiliary-proof, and selected-coin slots in a numbered composition block.

    Instances For
      source
      def Cslib.PCP.Encoded.Graph.composeSelectedTabulated {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) (g : Graph (α → α → Bool)) :
      Graph (Bool × (Fin 6 → Bool) → Bool × (Fin 6 → Bool) → Bool)

      Compile the selected tester and materialize the constraints over its 128-symbol alphabet.

      Instances For
        source
        theorem Cslib.PCP.Encoded.Graph.isPolyTime_composeSelectedTabulated {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} {Input : Type} {input : Input ↪ List Bool} {graph : Input → Graph (α → α → Bool)} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))) (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) :
        Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => composeSelectedTabulated number coins queries (graph x)) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

        The shared compiler charges the graph, every selected query, and the full output tables.

        source
        @[simp]
        theorem Cslib.PCP.Encoded.Graph.vertices_composeSelectedTabulated {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) (g : Graph (α → α → Bool)) :
        (composeSelectedTabulated number coins queries g).vertices = (g.vertices + g.edges.length) * width

        The output reserves a fixed block for each old vertex and edge.

        source
        @[simp]
        theorem Cslib.PCP.Encoded.Graph.length_edges_composeSelectedTabulated {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) (g : Graph (α → α → Bool)) :
        (composeSelectedTabulated number coins queries g).edges.length = g.edges.length * coins.length * queries.length

        Every listed coin and query contributes one occurrence for each old edge.

        source
        theorem Cslib.PCP.Encoded.Graph.WellFormed.composeSelectedTabulated {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) {g : Graph (α → α → Bool)} (hg : g.WellFormed) :
        (Graph.composeSelectedTabulated number coins queries g).WellFormed

        Selected composition preserves endpoint bounds for arbitrary supplied coin and query lists.

        source
        theorem Cslib.PCP.Encoded.Graph.unsatVal_composeSelectedTabulated_eq {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : Fin 5 × HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : Fin 6), i ∈ queries) :
        ((composeSelectedTabulated number coins queries g).toGraph id).unsatVal = (g.toGraph id).composeSelected.unsatVal

        Complete enumeration gives exactly the value of mathematical selected composition.

        source
        theorem Cslib.PCP.Encoded.Graph.satisfiable_composeSelectedTabulated_iff {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} [Nonempty α] (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : Fin 5 × HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : Fin 6), i ∈ queries) :
        ((composeSelectedTabulated number coins queries g).toGraph id).Satisfiable ↔ (g.toGraph id).Satisfiable

        Complete selected composition preserves satisfiability.

        source
        theorem Cslib.PCP.Encoded.Graph.le_unsatVal_composeSelectedTabulated {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} [Nonempty α] (number : SelectedComposeSlot α ≃ Fin width) (coins : List (Fin 5 × HadamardTester.Rand α)) (queries : List (Fin 6)) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : Fin 5 × HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : Fin 6), i ∈ queries) :
        (g.toGraph id).unsatVal / 840 ≤ ((composeSelectedTabulated number coins queries g).toGraph id).unsatVal

        The six-query gadget retains at least 1/840 of the input's unsatisfied fraction.