Executable composition with the Hadamard assignment tester

Composition replaces each original edge by the tester's coin-to-query edges. Supplied finite numberings give disjoint identifiers to input-table bits, proof-table bits, and coin vertices. Explicit lists enumerate coins and queries; the exact interpretation and soundness results require each list to enumerate its type once. The program itself also handles empty or incomplete lists, and preserves endpoint bounds for every well-formed input graph.

The alphabet, its numbering, and the coin/query lists are fixed independently of the input graph. The uniform polynomial-time certificate charges graph enumeration, tester queries, copying, and output storage. These constants can be enormous: this establishes asymptotic constructibility, not a practical bound on the size of a fully expanded tester gadget.

composeTabulated materializes each output constraint as a Boolean table over the fixed answer alphabet. Its certificate hides internal coin/query encodings and composes with a graph routine written in the client's input representation.

Main definitions

• Cslib.PCP.Encoded.Graph.compose: executable gadget enumeration and vertex numbering.
• Cslib.PCP.Encoded.Graph.composeTabulated: composition with tabulated output constraints.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_composeTabulated: uniform, compositional cost certificate.
• Cslib.PCP.Encoded.Graph.toGraph_compose: exact agreement with mathematical composition.
• Cslib.PCP.Encoded.Graph.le_unsatVal_compose: the existing 1/476 gap bound transfers.
• Cslib.PCP.Encoded.Graph.satisfiable_composeTabulated_iff: satisfiability is preserved.

References

• I. Dinur, The PCP theorem by gap amplification
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.PCP.Encoded.HadamardTester.implementation {α : Type} [Fintype α] [DecidableEq α] : AssignmentTester.Implementation α (α → Bool) (HadamardTester.LinPos α ⊕ HadamardTester.QuadPos α) (HadamardTester.Rand α) HadamardTester.Query Bool

Executable conjunction tester data used by the legacy composition API.

theorem Cslib.PCP.Encoded.HadamardTester.realizes_implementation {α : Type} [Fintype α] [DecidableEq α] : implementation.Realizes HadamardTester.assignmentTester

The executable conjunction tester implements the mathematical assignment tester exactly.

@[reducible, inline]

abbrev Cslib.PCP.Encoded.Graph.ComposeSlot (α : Type) : Type

The local slots in one numbered block: an input-table bit, a proof-table bit, or a coin vertex. The block's owner is the old vertex or edge index.

def Cslib.PCP.Encoded.Graph.composePosition {α : Type} {width : ℕ} (number : ComposeSlot α ≃ Fin width) (edge src dst : ℕ) : HadamardTester.Pos α → ℕ

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

def Cslib.PCP.Encoded.Graph.composeEdge {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (edge : Edge (α → α → Bool)) (index : ℕ) (coins : HadamardTester.Rand α) (i : HadamardTester.Query) : Edge ((α → α → Bool) × HadamardTester.Rand α × HadamardTester.Query)

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

def Cslib.PCP.Encoded.Graph.composeEval {α : Type} [Fintype α] [DecidableEq α] (descriptor : (α → α → Bool) × HadamardTester.Rand α × HadamardTester.Query) (a b : Bool × (HadamardTester.Query → Bool)) : Bool

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

def Cslib.PCP.Encoded.Graph.composeDarts {α : Type} (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) : List ((ℕ × HadamardTester.Rand α) × HadamardTester.Query)

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

def Cslib.PCP.Encoded.Graph.compose {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) : Graph ((α → α → Bool) × HadamardTester.Rand α × HadamardTester.Query)

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.Encoded.Graph.isPolyTime_composePosition {α Input : Type} {input : Input ↪ List Bool} {width : ℕ} [Finite α] (number : ComposeSlot α ≃ Fin width) {edge src dst : Input → ℕ} {position : Input → HadamardTester.Pos α} {positionEncoding : HadamardTester.Pos α ↪ 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.Encoded.Graph.isPolyTime_composeEdge {α Input : Type} [Fintype α] [DecidableEq α] {input : Input ↪ List Bool} {width : ℕ} (number : ComposeSlot α ≃ Fin width) {edge : Input → Edge (α → α → Bool)} {index : Input → ℕ} {coins : Input → HadamardTester.Rand α} {query : Input → HadamardTester.Query} {coinsEncoding : HadamardTester.Rand α ↪ List Bool} {queryEncoding : HadamardTester.Query ↪ List Bool} (hedge : Turing.MultiTapeTM.ComputableTidilyInPolyTime edge input (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) => composeEdge number (edge x) (index x) (coins x) (query x)) input (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.Encoded.Graph.isPolyTime_composeEval {α : Type} [Fintype α] [DecidableEq α] (coinsEncoding : HadamardTester.Rand α ↪ List Bool) (queryEncoding : HadamardTester.Query ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ((α → α → Bool) × HadamardTester.Rand α × HadamardTester.Query) × (Bool × (HadamardTester.Query → Bool)) × Bool × (HadamardTester.Query → Bool)) => 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 Turing.MultiTapeTM.encBool (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))) Turing.MultiTapeTM.encBool

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

theorem Cslib.PCP.Encoded.Graph.isPolyTime_compose {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (coinsEncoding : HadamardTester.Rand α ↪ List Bool) (queryEncoding : HadamardTester.Query ↪ List Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (compose number coins queries) (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool))) (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.Encoded.Graph.composeTabulated {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) : Graph (Bool × (HadamardTester.Query → Bool) → Bool × (HadamardTester.Query → Bool) → Bool)

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

theorem Cslib.PCP.Encoded.Graph.isPolyTime_composeTabulated {α Input : Type} [Fintype α] [DecidableEq α] {input : Input ↪ List Bool} {width : ℕ} {graph : Input → Graph (α → α → Bool)} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding (Turing.MultiTapeTM.encPi (Turing.MultiTapeTM.encPi Turing.MultiTapeTM.encBool)))) (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => composeTabulated number coins queries (graph x)) input (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.Encoded.Graph.length_edges_compose {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) : (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.Encoded.Graph.vertices_compose {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) : (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.Encoded.Graph.composeOwner {α E : Type} (index : E → ℕ) : ConstraintGraph.ComposePos ℕ E α ⊕ E × HadamardTester.Rand α → ℕ × ComposeSlot α

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

def Cslib.PCP.Encoded.Graph.composeVertex {α : Type} {width : ℕ} {E : Type} (number : ComposeSlot α ≃ Fin width) (index : E → ℕ) (vertex : ConstraintGraph.ComposePos ℕ E α ⊕ E × HadamardTester.Rand α) : ℕ

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

theorem Cslib.PCP.Encoded.Graph.composeVertex_injective {α : Type} {width : ℕ} {E : Type} (number : ComposeSlot α ≃ 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.Encoded.Graph.composePosition_eq {α : Type} {width : ℕ} (number : ComposeSlot α ≃ Fin width) (g : Graph (α → α → Bool)) (e : Fin g.edges.length) (p : HadamardTester.Pos α) : composePosition number (↑e) (g.edges.get e).src (g.edges.get e).dst p = composeVertex number Fin.val (Sum.inl ((g.toGraph id).testerPos e p))

The explicit endpoint selection agrees with ConstraintGraph.testerPos.

@[simp]

theorem Cslib.PCP.Encoded.Graph.mem_composeDarts_iff {α : Type} (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (p : (ℕ × HadamardTester.Rand α) × HadamardTester.Query) : 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.Encoded.Graph.WellFormed.compose {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) {g : Graph (α → α → Bool)} (hg : g.WellFormed) : (Graph.compose number coins queries g).WellFormed

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

theorem Cslib.PCP.Encoded.Graph.nodup_composeDarts {α : Type} (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : 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.Encoded.Graph.composeEnumeration {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : HadamardTester.Query), i ∈ queries) : (compose number coins queries g).edges.Enumeration fun (p : (Fin g.edges.length × HadamardTester.Rand α) × HadamardTester.Query) => composeEdge number (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.Encoded.Graph.toGraph_compose {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : HadamardTester.Query), i ∈ queries) : (compose number coins queries g).toGraph composeEval = ((g.toGraph id).compose.map (composeVertex number Fin.val)).comap ⇑(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.Encoded.Graph.unsatVal_compose_eq {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : HadamardTester.Query), i ∈ queries) : ((compose number coins queries g).toGraph composeEval).unsatVal = (g.toGraph id).compose.unsatVal

Exact interpretation and injective numbering preserve the mathematical composition value.

theorem Cslib.PCP.Encoded.Graph.satisfiable_compose_iff {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} [Nonempty α] (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : HadamardTester.Query), i ∈ queries) : ((compose number coins queries g).toGraph composeEval).Satisfiable ↔ (g.toGraph id).Satisfiable

Full executable composition preserves satisfiability.

theorem Cslib.PCP.Encoded.Graph.le_unsatVal_compose {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} [Nonempty α] (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : HadamardTester.Query), i ∈ queries) : (g.toGraph id).unsatVal / 476 ≤ ((compose number coins queries g).toGraph composeEval).unsatVal

Full executable composition retains at least the existing 1/476 fraction of the gap.

theorem Cslib.PCP.Encoded.Graph.unsatVal_composeTabulated_eq {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : HadamardTester.Query), i ∈ queries) : ((composeTabulated number coins queries g).toGraph id).unsatVal = (g.toGraph id).compose.unsatVal

Tabulating the output constraints preserves the exact mathematical composition value.

theorem Cslib.PCP.Encoded.Graph.satisfiable_composeTabulated_iff {α : Type} [Fintype α] [DecidableEq α] {width : ℕ} [Nonempty α] (number : ComposeSlot α ≃ Fin width) (coins : List (HadamardTester.Rand α)) (queries : List HadamardTester.Query) (g : Graph (α → α → Bool)) (hcoins : coins.Nodup) (hqueries : queries.Nodup) (hmemCoins : ∀ (ω : HadamardTester.Rand α), ω ∈ coins) (hmemQueries : ∀ (i : HadamardTester.Query), i ∈ queries) : ((composeTabulated number coins queries g).toGraph id).Satisfiable ↔ (g.toGraph id).Satisfiable

Tabulated full composition preserves satisfiability.