Documentation

Complexity.Computability.PCP.Encoded.Composition.Enumeration

Complete enumeration for executable composition #

Constructive finite enumerations supply the assignment tester's slot numbering, coins, and queries. The alphabet is fixed; the graph remains runtime input. Composition preserves the existing exact interpretation and charges all intermediate and output constraint tables. The fixed enumerations and tables can be enormous; the certificate is asymptotic in graph size, not a claim of practical runtime at arbitrary fixed alphabets.

Main definitions #

Main results #

References #

source
@[instance_reducible]
def Cslib.PCP.Encoded.Graph.ComposeSlot.finEnum (α : Type) [FinEnum α] :
FinEnum (ComposeSlot α)

Constructively number the input, proof, and coin slots of one assignment-tester block.

Instances For
    source
    def Cslib.PCP.Encoded.Graph.composeEnumerated {α : Type} [FinEnum α] (g : Graph (α → α → Bool)) :
    Graph (Bool × (HadamardTester.Query → Bool) → Bool × (HadamardTester.Query → Bool) → Bool)

    Apply every assignment-tester coin and query, then tabulate the output constraints.

    Instances For
      source
      theorem Cslib.PCP.Encoded.Graph.isPolyTime_composeEnumerated {α : Type} [FinEnum α] {Input : Type} {input : Input ↪ List Bool} {constraintEncoding : (α → α → Bool) ↪ List Bool} {graph : Input → Graph (α → α → Bool)} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding constraintEncoding)) :
      Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (graph x).composeEnumerated) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

      Compose a certified runtime graph, charging a conversion from its fixed constraint encoding and every output table. The input need not use the implementation's finite enumeration.

      source
      @[simp]
      theorem Cslib.PCP.Encoded.Graph.vertices_composeEnumerated {α : Type} [FinEnum α] (g : Graph (α → α → Bool)) :
      g.composeEnumerated.vertices = (g.vertices + g.edges.length) * Fintype.card (ComposeSlot α)

      The declared vertex count includes the complete input, proof, and coin slots.

      source
      @[simp]
      theorem Cslib.PCP.Encoded.Graph.length_edges_composeEnumerated {α : Type} [FinEnum α] (g : Graph (α → α → Bool)) :
      g.composeEnumerated.edges.length = g.edges.length * Fintype.card (HadamardTester.Rand α) * Fintype.card HadamardTester.Query

      Each original edge contributes one edge per coin and query pair.

      source
      theorem Cslib.PCP.Encoded.Graph.WellFormed.composeEnumerated {α : Type} [FinEnum α] {g : Graph (α → α → Bool)} (hg : g.WellFormed) :
      g.composeEnumerated.WellFormed

      Valid input endpoints give valid endpoints in the completely enumerated gadget graph.

      source
      theorem Cslib.PCP.Encoded.Graph.unsatVal_composeEnumerated_eq {α : Type} [FinEnum α] (g : Graph (α → α → Bool)) :
      (g.composeEnumerated.toGraph id).unsatVal = (g.toGraph id).compose.unsatVal

      Complete constructive enumeration preserves the exact mathematical composition value.

      source
      theorem Cslib.PCP.Encoded.Graph.satisfiable_composeEnumerated_iff {α : Type} [FinEnum α] [Nonempty α] (g : Graph (α → α → Bool)) :
      (g.composeEnumerated.toGraph id).Satisfiable ↔ (g.toGraph id).Satisfiable

      Complete tabulated composition preserves satisfiability.

      source
      theorem Cslib.PCP.Encoded.Graph.le_unsatVal_composeEnumerated {α : Type} [FinEnum α] [Nonempty α] (g : Graph (α → α → Bool)) :
      (g.toGraph id).unsatVal / 476 ≤ (g.composeEnumerated.toGraph id).unsatVal

      Complete tabulated composition retains the tester's 1/476 fraction of the input value.