Complete enumeration for selected composition

The selected tester uses the shared complete-enumeration compiler. Its coins add a choice of one of five checks to the Hadamard product coins, and its queries are indexed by Fin 6. All finite enumerations are fixed with the alphabet; the graph and its tables remain charged runtime data.

Main definitions

• Cslib.PCP.Encoded.Graph.composeSelectedEnumerated: complete selected composition.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_composeSelectedEnumerated: the construction certificate.
• Cslib.PCP.Encoded.Graph.satisfiable_composeSelectedEnumerated_iff: satisfiability transfer.
• Cslib.PCP.Encoded.Graph.le_unsatVal_composeSelectedEnumerated: retention of 1/840 of value.

References

• I. Dinur, The PCP theorem by gap amplification

@[instance_reducible]

def Cslib.PCP.Encoded.Graph.SelectedComposeSlot.finEnum (α : Type) [FinEnum α] : FinEnum (SelectedComposeSlot α)

Constructively number all input, proof, and selected-coin slots.

def Cslib.PCP.Encoded.Graph.composeSelectedEnumerated {α : Type} [FinEnum α] (g : Graph (α → α → Bool)) : Graph (SelectedAlphabet → SelectedAlphabet → Bool)

Run every selected check and query, then materialize the output constraints.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_composeSelectedEnumerated {α : Type} [FinEnum α] {Input : Type} {input : Input ↪ List Bool} {constraintEncoding : (α → α → Bool) ↪ List Bool} {graph : Input → Graph (α → α → Bool)} (hgraph : Turing.MultiTapeTM.ComputableInPolyTime graph input (encoding constraintEncoding)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (graph x).composeSelectedEnumerated) input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

Selected composition accepts any certified input-constraint encoding.

@[simp]

theorem Cslib.PCP.Encoded.Graph.vertices_composeSelectedEnumerated {α : Type} [FinEnum α] (g : Graph (α → α → Bool)) : g.composeSelectedEnumerated.vertices = (g.vertices + g.edges.length) * Fintype.card (SelectedComposeSlot α)

Each old vertex and edge reserves a complete local slot block.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_edges_composeSelectedEnumerated {α : Type} [FinEnum α] (g : Graph (α → α → Bool)) : g.composeSelectedEnumerated.edges.length = g.edges.length * Fintype.card (Fin 5 × HadamardTester.Rand α) * 6

Each old edge occurs once for every selected coin and query pair.

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

Complete selected composition preserves endpoint bounds.

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

Complete selected composition preserves satisfiability.

theorem Cslib.PCP.Encoded.Graph.le_unsatVal_composeSelectedEnumerated {α : Type} [FinEnum α] [Nonempty α] (g : Graph (α → α → Bool)) : (g.toGraph id).unsatVal / 840 ≤ (g.composeSelectedEnumerated.toGraph id).unsatVal

The compiled selected tester retains 1/840 of the input value.