Executable composition from a realized assignment tester

An AssignmentTester.Implementation supplies executable queries and acceptance for runtime Boolean constraints. Implementation.Realizes certifies their exact mathematical interpretation. One generator enumerates the coin-to-query edges for any such realization. The fixed finite types, numbering, and coin/query lists are independent of the runtime graph. Its certificates charge graph enumeration, all tables, copies, and output storage; they do not give alphabet-uniform or practical bounds.

Main definitions

• Cslib.PCP.AssignmentTester.Implementation: executable data interpreting a mathematical tester.
• Cslib.PCP.AssignmentTester.Implementation.compose: the numbered gadget graph.
• Cslib.PCP.AssignmentTester.Implementation.composeTabulated: its tabulated constraints.

Main results

• Cslib.PCP.AssignmentTester.Implementation.toGraph_compose: exact interpretation.
• Cslib.PCP.AssignmentTester.Implementation.isPolyTime_composeTabulated: construction certificate.
• Cslib.PCP.AssignmentTester.Implementation.unsatVal_composeTabulated_eq: exact value transfer.

References

• I. Dinur, The PCP theorem by gap amplification

@[reducible, inline]

abbrev Cslib.PCP.AssignmentTester.ComposeSlot (I P R : Type) : Type

The local input, auxiliary, and coin slots in a numbered gadget block.

structure Cslib.PCP.AssignmentTester.Implementation (α I P R Q Γ : Type) : Type

Executable queries and decisions for runtime Boolean constraints. Correctness relative to a mathematical tester is the separate proposition Implementation.Realizes.

• query : (α → α → Bool) → R → Q → Fin 2 × I ⊕ P

  Compute one queried input or auxiliary position.

• accepts : (α → α → Bool) → R → (Q → Γ) → Bool

  Decide acceptance from the supplied query answers.

structure Cslib.PCP.AssignmentTester.Implementation.Realizes {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) (T : AssignmentTester α I P R Q Γ) : Prop

Exact agreement with a mathematical tester, kept separate from executable data so that noncomputable mathematical definitions are absent from compiled generator arguments.

• query_eq (constraint : α → α → Bool) (coins : R) (i : Q) : impl.query constraint coins i = (T.test fun (a b : α) => constraint a b = true).query coins i

  Computed positions agree with the mathematical tester.

• accepts_eq_true (constraint : α → α → Bool) (coins : R) (answers : Q → Γ) : impl.accepts constraint coins answers = true ↔ (T.test fun (a b : α) => constraint a b = true).Accepts coins answers

  Computed decisions agree with the mathematical acceptance predicate.

def Cslib.PCP.AssignmentTester.Implementation.composePosition {I P R : Type} {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (edge src dst : ℕ) : Fin 2 × I ⊕ P → ℕ

Number a queried proof position using a supplied finite slot numbering.

def Cslib.PCP.AssignmentTester.Implementation.composeEdge {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (edge : Encoded.Edge (α → α → Bool)) (index : ℕ) (coins : R) (i : Q) : Encoded.Edge ((α → α → Bool) × R × Q)

Build the edge from one coin vertex to one of the queried proof positions.

def Cslib.PCP.AssignmentTester.Implementation.composeEval {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) [BEq Γ] (descriptor : (α → α → Bool) × R × Q) (a b : Γ × (Q → Γ)) : Bool

Verify the claimed answers and their agreement with the queried proof symbol.

def Cslib.PCP.AssignmentTester.Implementation.composeDarts {α R Q : Type} (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) : List ((ℕ × R) × Q)

Enumerate all supplied random strings and queries for every original edge, in list order.

def Cslib.PCP.AssignmentTester.Implementation.compose {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) : Encoded.Graph ((α → α → Bool) × R × Q)

Compose an encoded graph with a specified list of coins and queries. Full alphabet reduction requires each of those lists to enumerate its type exactly once.

theorem Cslib.PCP.AssignmentTester.Implementation.isPolyTime_composePosition {I P R Input : Type} {input : Input ↪ List Bool} {width : ℕ} [Finite I] [Finite P] (number : ComposeSlot I P R ≃ Fin width) {edge src dst : Input → ℕ} {position : Input → Fin 2 × I ⊕ P} {positionEncoding : Fin 2 × I ⊕ P ↪ List Bool} (hedge : Turing.MultiTapeTM.ComputableTidilyInPolyTime edge input Turing.MultiTapeTM.encUnary) (hsrc : Turing.MultiTapeTM.ComputableTidilyInPolyTime src input Turing.MultiTapeTM.encUnary) (hdst : Turing.MultiTapeTM.ComputableTidilyInPolyTime dst input Turing.MultiTapeTM.encUnary) (hposition : Turing.MultiTapeTM.ComputableTidilyInPolyTime position input positionEncoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => composePosition number (edge x) (src x) (dst x) (position x)) input Turing.MultiTapeTM.encUnary

Position numbering charges all runtime indices; finite dispatch only concerns the fixed alphabet's local proof position.

theorem Cslib.PCP.AssignmentTester.Implementation.isPolyTime_composeEdge {α I P R Q Γ Input : Type} (impl : Implementation α I P R Q Γ) {input : Input ↪ List Bool} {width : ℕ} [Fintype α] [Finite I] [Finite P] [Finite R] [Finite Q] (number : ComposeSlot I P R ≃ Fin width) {edge : Input → Encoded.Edge (α → α → Bool)} {index : Input → ℕ} {coins : Input → R} {query : Input → Q} {coinsEncoding : R ↪ List Bool} {queryEncoding : Q ↪ List Bool} (hedge : Turing.MultiTapeTM.ComputableTidilyInPolyTime edge input (Encoded.Edge.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) (hcoins : Turing.MultiTapeTM.ComputableTidilyInPolyTime coins input coinsEncoding) (hquery : Turing.MultiTapeTM.ComputableTidilyInPolyTime query input queryEncoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => impl.composeEdge number (edge x) (index x) (coins x) (query x)) input (Encoded.Edge.encoding (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair coinsEncoding queryEncoding)))

A gadget edge is computed uniformly in the original edge, its index, coins, and query.

theorem Cslib.PCP.AssignmentTester.Implementation.isPolyTime_composeEval {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) [Fintype α] [Fintype Q] [Finite R] [Finite Γ] [BEq Γ] (symbolEncoding : Γ ↪ List Bool) (coinsEncoding : R ↪ List Bool) (queryEncoding : Q ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ((α → α → Bool) × R × Q) × (Γ × (Q → Γ)) × Γ × (Q → Γ)) => impl.composeEval p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair coinsEncoding queryEncoding)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair symbolEncoding (Turing.MultiTapeTM.encPi symbolEncoding)) (Turing.MultiTapeTM.encPair symbolEncoding (Turing.MultiTapeTM.encPi symbolEncoding)))) Turing.MultiTapeTM.encBool

The verifier's edge predicate charges all supplied finite tables and query answers.

theorem Cslib.PCP.AssignmentTester.Implementation.isPolyTime_compose {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} [Fintype α] [Finite I] [Finite P] [Finite R] [Finite Q] (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (coinsEncoding : R ↪ List Bool) (queryEncoding : Q ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (impl.compose number coins queries) (Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) (Encoded.Graph.encoding (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair coinsEncoding queryEncoding)))

The full construction charges the old graph, enumeration, each tester call, copying, and the complete output graph. The finite alphabet and supplied lists are fixed.

def Cslib.PCP.AssignmentTester.Implementation.composeTabulated {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} [BEq Γ] (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) : Encoded.Graph (Γ × (Q → Γ) → Γ × (Q → Γ) → Bool)

Return composition to the fixed Boolean-table descriptor type over its answer alphabet.

theorem Cslib.PCP.AssignmentTester.Implementation.isPolyTime_composeTabulated {α I P R Q Γ Input : Type} (impl : Implementation α I P R Q Γ) {input : Input ↪ List Bool} {width : ℕ} [Fintype α] [Finite I] [Finite P] [Finite R] [Fintype Q] [DecidableEq Q] [Fintype Γ] [BEq Γ] {graph : Input → Encoded.Graph (α → α → Bool)} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))) (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => impl.composeTabulated number coins queries (graph x)) input (Encoded.Graph.encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))

Tabulated composition fixes its internal finite encodings, so clients only certify the input graph in their own input representation. Every output constraint table is charged.

@[simp]

theorem Cslib.PCP.AssignmentTester.Implementation.length_edges_compose {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) : (impl.compose number coins queries g).edges.length = g.edges.length * coins.length * queries.length

Each original edge produces one edge for every supplied pair of coins and query.

@[simp]

theorem Cslib.PCP.AssignmentTester.Implementation.vertices_compose {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) : (impl.compose number coins queries g).vertices = (g.vertices + g.edges.length) * width

The declared vertex count grows by a fixed factor in the old vertices and edges.

def Cslib.PCP.AssignmentTester.Implementation.composeOwner {I P R E : Type} (index : E → ℕ) : ComposePos ℕ E I P ⊕ E × R → ℕ × ComposeSlot I P R

Split a mathematical composed vertex into its owner index and local slot.

def Cslib.PCP.AssignmentTester.Implementation.composeVertex {I P R : Type} {width : ℕ} {E : Type} (number : ComposeSlot I P R ≃ Fin width) (index : E → ℕ) (vertex : ComposePos ℕ E I P ⊕ E × R) : ℕ

The same explicit numbering on all mathematical proof positions and coin vertices.

theorem Cslib.PCP.AssignmentTester.Implementation.composeVertex_injective {I P R : Type} {width : ℕ} [Nonempty R] {E : Type} (number : ComposeSlot I P R ≃ Fin width) {index : E → ℕ} (hindex : Function.Injective index) : Function.Injective (composeVertex number index)

Distinct table positions and coin vertices retain distinct identifiers.

theorem Cslib.PCP.AssignmentTester.Implementation.composePosition_eq {α I P R : Type} {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (g : Encoded.Graph (α → α → Bool)) (e : Fin g.edges.length) (p : Fin 2 × I ⊕ P) : composePosition number (↑e) (g.edges.get e).src (g.edges.get e).dst p = composeVertex number Fin.val (Sum.inl (testerPos (g.toGraph id) e p))

The explicit endpoint selection agrees with ConstraintGraph.testerPos.

@[simp]

theorem Cslib.PCP.AssignmentTester.Implementation.mem_composeDarts_iff {α R Q : Type} (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (p : (ℕ × R) × Q) : p ∈ composeDarts coins queries g ↔ p.1.1 < g.edges.length ∧ p.1.2 ∈ coins ∧ p.2 ∈ queries

The dart enumeration includes exactly the valid old indices and listed coins/queries.

theorem Cslib.PCP.AssignmentTester.Implementation.wellFormed_compose {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) {g : Encoded.Graph (α → α → Bool)} (hg : g.WellFormed) : (impl.compose number coins queries g).WellFormed

Valid old endpoints give valid output endpoints, even for empty or incomplete coin lists.

theorem Cslib.PCP.AssignmentTester.Implementation.nodup_composeDarts {α R Q : Type} (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) : (composeDarts coins queries g).Nodup

Listing each coin and query once lists each composed dart once.

noncomputable def Cslib.PCP.AssignmentTester.Implementation.composeEnumeration {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {width : ℕ} (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : R), ω ∈ coins) (hmemQueries : ∀ (i : Q), i ∈ queries) : (impl.compose number coins queries g).edges.Enumeration fun (p : (Fin g.edges.length × R) × Q) => impl.composeEdge number (Encoded.Graph.edgeAt (fun (x x_1 : α) => false) g ↑p.1.1) (↑p.1.1) p.1.2 p.2

Composition retains the ordered edge, coin and query occurrences, even when stored edge values coincide.

theorem Cslib.PCP.AssignmentTester.Implementation.toGraph_compose {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} {width : ℕ} (hreal : impl.Realizes T) [BEq Γ] [LawfulBEq Γ] (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : R), ω ∈ coins) (hmemQueries : ∀ (i : Q), i ∈ queries) : (impl.compose number coins queries g).toGraph impl.composeEval = ((T.compose (g.toGraph id)).map (composeVertex number Fin.val)).comap ⇑(impl.composeEnumeration number coins queries g hcoins hqueries hmemCoins hmemQueries).equiv

Enumerating every coin and query once gives exactly the existing composed graph, with the specified vertex numbering and the explicit output edge order.

theorem Cslib.PCP.AssignmentTester.Implementation.unsatVal_compose_eq {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} {width : ℕ} (hreal : impl.Realizes T) [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Γ] [BEq Γ] [LawfulBEq Γ] (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : R), ω ∈ coins) (hmemQueries : ∀ (i : Q), i ∈ queries) : ((impl.compose number coins queries g).toGraph impl.composeEval).unsatVal = (T.compose (g.toGraph id)).unsatVal

Exact interpretation and injective numbering preserve the mathematical composition value.

theorem Cslib.PCP.AssignmentTester.Implementation.satisfiable_compose_iff {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} {width : ℕ} (hreal : impl.Realizes T) [Fintype R] [Finite Q] [Nonempty R] [Nonempty Q] [Nonempty α] [Nonempty Γ] [BEq Γ] [LawfulBEq Γ] (hcomplete : T.IsComplete) {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (hδ : 0 < δ) (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : R), ω ∈ coins) (hmemQueries : ∀ (i : Q), i ∈ queries) : ((impl.compose number coins queries g).toGraph impl.composeEval).Satisfiable ↔ (g.toGraph id).Satisfiable

Full executable composition preserves satisfiability.

theorem Cslib.PCP.AssignmentTester.Implementation.le_unsatVal_compose {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} {width : ℕ} (hreal : impl.Realizes T) [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Q] [Nonempty Γ] [BEq Γ] [LawfulBEq Γ] {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (hδ : 0 < δ) (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : R), ω ∈ coins) (hmemQueries : ∀ (i : Q), i ∈ queries) : (g.toGraph id).unsatVal / (↑(Fintype.card Q) / δ) ≤ ((impl.compose number coins queries g).toGraph impl.composeEval).unsatVal

Executable composition retains the mathematical tester’s quantitative gap bound.

theorem Cslib.PCP.AssignmentTester.Implementation.unsatVal_composeTabulated_eq {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} {width : ℕ} (hreal : impl.Realizes T) [Fintype R] [Fintype Q] [Nonempty R] [Nonempty Γ] [BEq Γ] [LawfulBEq Γ] (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : R), ω ∈ coins) (hmemQueries : ∀ (i : Q), i ∈ queries) : ((impl.composeTabulated number coins queries g).toGraph id).unsatVal = (T.compose (g.toGraph id)).unsatVal

Tabulating the output constraints preserves the exact mathematical composition value.

theorem Cslib.PCP.AssignmentTester.Implementation.satisfiable_composeTabulated_iff {α I P R Q Γ : Type} (impl : Implementation α I P R Q Γ) {T : AssignmentTester α I P R Q Γ} {width : ℕ} (hreal : impl.Realizes T) [Fintype R] [Finite Q] [Nonempty R] [Nonempty Q] [Nonempty α] [Nonempty Γ] [BEq Γ] [LawfulBEq Γ] (hcomplete : T.IsComplete) {decode : (I → Γ) → α} {δ : ℝ} (hsound : T.Sound decode δ) (hδ : 0 < δ) (number : ComposeSlot I P R ≃ Fin width) (coins : List R) (queries : List Q) (g : Encoded.Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : R), ω ∈ coins) (hmemQueries : ∀ (i : Q), i ∈ queries) : ((impl.composeTabulated number coins queries g).toGraph id).Satisfiable ↔ (g.toGraph id).Satisfiable

Tabulated full composition preserves satisfiability.