Documentation

Complexity.Computability.PCP.Encoded.AssignmentTester

Executable Hadamard assignment testing #

A constraint given as a Boolean table determines the same assignment tester as PCP.hadamardTester, with executable queries and acceptance. Compatibility is decided by enumerating the finitely many assignments to the two ends. The remaining query operations and the five checks reuse the mathematical tester's computational definitions.

The alphabet is fixed independently of the runtime input. The finite input and output types therefore give polynomial-time certificates for the explicit algorithms. These certificates do not assert uniform polynomial dependence on the alphabet size, and no decoding choice occurs in the executable definitions.

Main definitions #

Main results #

References #

source
def Cslib.PCP.Encoded.HadamardTester.compatible {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (p q : Fin 2 × α) :
Bool

Decide compatibility by checking every assignment to the two endpoint variables.

Instances For
    source
    @[simp]
    theorem Cslib.PCP.Encoded.HadamardTester.compatible_eq_true {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (p q : Fin 2 × α) :
    compatible constraint p q = true ↔ HadamardTester.Compatible (fun (a b : α) => constraint a b = true) p q

    The executable check expresses the original existential compatibility condition.

    source
    def Cslib.PCP.Encoded.HadamardTester.equationCoeff {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) :
    (Fin 2 × α) × Fin 2 × α ⊕ Fin 2 → (Fin 2 × α) × Fin 2 × α → Bool

    The quadratic system of a Boolean constraint, computed by finite compatibility checks.

    Instances For
      source
      theorem Cslib.PCP.Encoded.HadamardTester.equationCoeff_eq {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) :
      equationCoeff constraint = PCP.HadamardTester.equationCoeff fun (a b : α) => constraint a b = true

      The executable coefficients agree exactly with the original quadratic system.

      source
      def Cslib.PCP.Encoded.HadamardTester.localTest {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) :
      LocalTest (HadamardTester.Pos α) (HadamardTester.Rand α) HadamardTester.Query Bool

      Run the existing five checks, supplying the executable quadratic coefficients.

      Instances For
        source
        theorem Cslib.PCP.Encoded.HadamardTester.localTest_eq {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) :
        localTest constraint = hadamardTester fun (a b : α) => constraint a b = true

        Equality of the entire test transfers its existing completeness and soundness theorems.

        source
        def Cslib.PCP.Encoded.HadamardTester.query {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : HadamardTester.Rand α) (i : HadamardTester.Query) :
        HadamardTester.Pos α

        The queried proof position for a specified constraint, random string, and query number.

        Instances For
          source
          def Cslib.PCP.Encoded.HadamardTester.accepts {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : HadamardTester.Rand α) (answers : HadamardTester.Query → Bool) :
          Bool

          The Boolean acceptance decision on the symbols claimed at the seventeen queries.

          Instances For
            source
            theorem Cslib.PCP.Encoded.HadamardTester.query_eq {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : HadamardTester.Rand α) (i : HadamardTester.Query) :
            query constraint coins i = (hadamardTester fun (a b : α) => constraint a b = true).query coins i

            Every computed position is the position specified by the mathematical assignment tester.

            source
            @[simp]
            theorem Cslib.PCP.Encoded.HadamardTester.accepts_eq_true {α : Type} [Fintype α] [DecidableEq α] (constraint : α → α → Bool) (coins : HadamardTester.Rand α) (answers : HadamardTester.Query → Bool) :
            accepts constraint coins answers = true ↔ (hadamardTester fun (a b : α) => constraint a b = true).Accepts coins answers

            The Boolean decision accepts exactly the answers accepted by the mathematical tester.

            source
            theorem Cslib.PCP.Encoded.HadamardTester.isPolyTime_query {α : Type} [Fintype α] [DecidableEq α] (coinsEncoding : HadamardTester.Rand α ↪ List Bool) (queryEncoding : HadamardTester.Query ↪ List Bool) (positionEncoding : HadamardTester.Pos α ↪ List Bool) :
            Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (α → α → Bool) × HadamardTester.Rand α × HadamardTester.Query) => query p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair coinsEncoding queryEncoding)) positionEncoding

            Fixed-alphabet query generation is uniform in the runtime constraint and random string.

            source
            theorem Cslib.PCP.Encoded.HadamardTester.isPolyTime_accepts {α : Type} [Fintype α] [DecidableEq α] (coinsEncoding : HadamardTester.Rand α ↪ List Bool) :
            Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (α → α → Bool) × HadamardTester.Rand α × (HadamardTester.Query → Bool)) => accepts p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair coinsEncoding (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool

            Fixed-alphabet acceptance charges the supplied constraint, coins, and all query answers.