Complete enumeration for executable assignment testers

Constructive finite enumerations supply a tester implementation's slot numbering, coins, and queries. The compiler charges all materialized constraint tables and retains edge occurrences. The alphabets and enumerations are fixed; polynomial time is uniform in the input graph.

Main definitions

• Cslib.PCP.AssignmentTester.Implementation.composeEnumerated: fully enumerated composition.

Main results

• Cslib.PCP.AssignmentTester.Implementation.isPolyTime_composeEnumerated: compositional certification from any fixed input-constraint encoding.
• Cslib.PCP.AssignmentTester.Implementation.unsatVal_composeEnumerated_eq: exact interpretation.
• Cslib.PCP.AssignmentTester.Implementation.satisfiable_composeEnumerated_iff: satisfiability transfer under the tester's completeness and soundness contracts.

References

• I. Dinur, The PCP theorem by gap amplification

def Cslib.PCP.AssignmentTester.Implementation.composeEnumerated {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) (g : Encoded.Graph (α → α → Bool)) : Encoded.Graph (Γ × (Q → Γ) → Γ × (Q → Γ) → Bool)

Apply every coin and query, then tabulate the output constraints over the answer alphabet.

theorem Cslib.PCP.AssignmentTester.Implementation.isPolyTime_composeEnumerated {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) [Finite α] [Fintype Γ] {Input : Type} {input : Input ↪ List Bool} {constraintEncoding : (α → α → Bool) ↪ List Bool} {graph : Input → Encoded.Graph (α → α → Bool)} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (Encoded.Graph.encoding constraintEncoding)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => impl.composeEnumerated (graph x)) input (Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

Charge the input-encoding conversion and every output table in completely enumerated composition. Input graphs need not use the implementation's own finite encoding.

@[simp]

theorem Cslib.PCP.AssignmentTester.Implementation.vertices_composeEnumerated {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) (g : Encoded.Graph (α → α → Bool)) : (impl.composeEnumerated g).vertices = (g.vertices + g.edges.length) * Fintype.card (ComposeSlot I P R)

Every old vertex and edge receives one complete local slot block.

@[simp]

theorem Cslib.PCP.AssignmentTester.Implementation.length_edges_composeEnumerated {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) (g : Encoded.Graph (α → α → Bool)) : (impl.composeEnumerated g).edges.length = g.edges.length * Fintype.card R * Fintype.card Q

Every old edge occurrence contributes one edge per coin and query pair.

theorem Cslib.PCP.AssignmentTester.Implementation.wellFormed_composeEnumerated {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) {g : Encoded.Graph (α → α → Bool)} (hg : g.WellFormed) : (impl.composeEnumerated g).WellFormed

Complete enumeration preserves endpoint bounds.

theorem Cslib.PCP.AssignmentTester.Implementation.unsatVal_composeEnumerated_eq {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} (hreal : impl.Realizes T) [Fintype R] [Fintype Q] [LawfulBEq Γ] [Nonempty R] [Nonempty Γ] (g : Encoded.Graph (α → α → Bool)) : ((impl.composeEnumerated g).toGraph id).unsatVal = (T.compose (g.toGraph id)).unsatVal

Complete enumeration preserves the exact value of the realized mathematical composition.

theorem Cslib.PCP.AssignmentTester.Implementation.satisfiable_composeEnumerated_iff {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} (hreal : impl.Realizes T) [Fintype R] [LawfulBEq Γ] [Nonempty R] [Nonempty Γ] [Nonempty α] [Nonempty Q] (hcomplete : T.IsComplete) {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (hδ : 0 < δ) (g : Encoded.Graph (α → α → Bool)) : ((impl.composeEnumerated g).toGraph id).Satisfiable ↔ (g.toGraph id).Satisfiable

Completeness and positive decoder soundness transfer satisfiability through the compiler.

theorem Cslib.PCP.AssignmentTester.Implementation.le_unsatVal_composeEnumerated {α I P R Q Γ : Type} [FinEnum I] [FinEnum P] [FinEnum R] [FinEnum Q] [BEq Γ] (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} (hreal : impl.Realizes T) [Fintype R] [Fintype Q] [LawfulBEq Γ] [Nonempty R] [Nonempty Γ] [Nonempty Q] {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (hδ : 0 < δ) (g : Encoded.Graph (α → α → Bool)) : (g.toGraph id).unsatVal / (↑(Fintype.card Q) / δ) ≤ ((impl.composeEnumerated g).toGraph id).unsatVal

Complete compilation retains the soundness loss of the supplied tester.