From a many-query test to a binary constraint graph

An assignment tester reads a handful of positions of its proof per random string, but a constraint graph checks two vertices per edge. The standard repair is to add a vertex for each random string, labelled by the answers the tester expects to see, and to connect it to each position it reads: the edge checks that the claimed answer matches the position's actual bit and that the claimed answers together pass the test. A rejecting random string then has at least one of its q edges violated — either the claimed answers fail the test outright, or they pass and so must disagree with the proof somewhere.

This module carries out that transformation for a family of tests indexed by a type E — one per edge of the outer graph, in the composition — over a shared set of positions. The edges of the result are the triples (e, z, i): test e, random string z, read i.

Main definitions

• Complexity.MultiTest — a family of many-query tests on a shared proof
• Complexity.MultiTest.toGraph — the binary constraint graph

Main results

• Complexity.MultiTest.card_rejects_le_card_unsatEdges — every rejecting random string accounts for a distinct violated edge
• Complexity.MultiTest.satisfiable_toGraph — a proof accepted everywhere gives a satisfying assignment

structure Complexity.MultiTest (Pos E Q : Type) : Type

A family of tests, indexed by E, reading a shared proof over positions Pos. A test uses R random bits, reads q positions chosen from its random string, and decides from the bits it read.

• R : ℕ

  The number of random bits.

• pos : E → BooleanAnalysis.Cube self.R → Q → Pos

  The positions read, indexed by Q, as a function of the test and its random string.

• check : E → BooleanAnalysis.Cube self.R → (Q → ZMod 2) → Bool

  The verdict, as a function of the bits read.

@[reducible, inline]

abbrev Complexity.MultiTest.Table (Pos : Type) : Type

A proof: one bit per position.

Equations

• Complexity.MultiTest.Table Pos = (Pos → ZMod 2)

def Complexity.MultiTest.accepts {Pos E Q : Type} (M : MultiTest Pos E Q) (T : Table Pos) (e : E) (z : BooleanAnalysis.Cube M.R) : Bool

Test e accepts the proof T on random string z.

Equations

• M.accepts T e z = M.check e z fun (i : Q) => T (M.pos e z i)

def Complexity.MultiTest.rejects {Pos E Q : Type} (M : MultiTest Pos E Q) (T : Table Pos) (e : E) : Finset (BooleanAnalysis.Cube M.R)

The random strings on which test e rejects T.

Equations

• M.rejects T e = {z : Complexity.BooleanAnalysis.Cube M.R | M.accepts T e z = false}

The binary graph

@[reducible, inline]

abbrev Complexity.MultiTest.Vert {Pos E Q : Type} (M : MultiTest Pos E Q) : Type

The vertices of the binary graph: the positions, and one vertex per (test, random string).

Equations

• M.Vert = (Pos ⊕ E × Complexity.BooleanAnalysis.Cube M.R)

@[reducible, inline]

abbrev Complexity.MultiTest.Edge {Pos E Q : Type} (M : MultiTest Pos E Q) : Type

The edges: one per (test, random string, read).

Equations

• M.Edge = (E × Complexity.BooleanAnalysis.Cube M.R × Q)

@[reducible, inline]

abbrev Complexity.MultiTest.Alpha (Q : Type) : Type

The alphabet: a bit (used at positions) paired with a tuple of claimed answers (used at test vertices).

Equations

• Complexity.MultiTest.Alpha Q = (ZMod 2 × (Q → ZMod 2))

@[instance_reducible, instance 2000]

noncomputable instance Complexity.MultiTest.instNumEncCube (n : ℕ) : NumEnc (BooleanAnalysis.Cube n)

A random string is numbered by its own enumeration: the number of random bits is a constant, so this is a lookup on a bounded key.

Equations

• Complexity.MultiTest.instNumEncCube n = Complexity.NumEnc.ofFintype (Complexity.BooleanAnalysis.Cube n)

noncomputable def Complexity.MultiTest.edgeOf {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype E] [Fintype Q] [NumEnc E] [NumEnc Q] (k : Fin (Fintype.card M.Edge)) : M.Edge

The edge a Fin index stands for.

Equations

• M.edgeOf k = (Complexity.NumEnc.equivFinCard M.Edge).symm k

noncomputable def Complexity.MultiTest.vertIdx {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [NumEnc Pos] [NumEnc E] (v : M.Vert) : Fin (Fintype.card M.Vert)

The Fin index of a vertex.

Equations

• M.vertIdx v = (Complexity.NumEnc.equivFinCard M.Vert) v

noncomputable def Complexity.MultiTest.toGraph {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] : ConstraintGraph (Alpha Q)

The binary constraint graph. Edge (e, z, i) runs from the test vertex (e, z) to the position pos e z i, and holds when the test vertex's claimed answers pass test e on z and its i-th claimed answer is the position's bit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.MultiTest.tableOf {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (A : M.toGraph.Assignment) : Table Pos

The proof an assignment of the binary graph carries at its positions.

Equations

• M.tableOf A p = (A (M.vertIdx (Sum.inl p))).1

theorem Complexity.MultiTest.satisfies_toGraph_iff {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (A : M.toGraph.Assignment) (k : Fin (Fintype.card M.Edge)) : M.toGraph.Satisfies A k ↔ M.check (M.edgeOf k).1 (M.edgeOf k).2.1 (A (M.vertIdx (Sum.inr ((M.edgeOf k).1, (M.edgeOf k).2.1)))).2 = true ∧ (A (M.vertIdx (Sum.inr ((M.edgeOf k).1, (M.edgeOf k).2.1)))).2 (M.edgeOf k).2.2 = M.tableOf A (M.pos (M.edgeOf k).1 (M.edgeOf k).2.1 (M.edgeOf k).2.2)

The constraint of edge (e, z, i), spelled out.

noncomputable def Complexity.MultiTest.edgeIdx {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype E] [Fintype Q] [NumEnc E] [NumEnc Q] (x : M.Edge) : Fin (Fintype.card M.Edge)

The Fin index of an edge.

Equations

• M.edgeIdx x = (Complexity.NumEnc.equivFinCard M.Edge) x

@[simp]

theorem Complexity.MultiTest.edgeOf_edgeIdx {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype E] [Fintype Q] [NumEnc E] [NumEnc Q] (x : M.Edge) : M.edgeOf (M.edgeIdx x) = x

theorem Complexity.MultiTest.exists_unsat_of_rejects {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] [Nonempty Q] (A : M.toGraph.Assignment) (e : E) (z : BooleanAnalysis.Cube M.R) (hz : z ∈ M.rejects (M.tableOf A) e) : ∃ (i : Q), ¬M.toGraph.Satisfies A (M.edgeIdx (e, z, i))

A rejecting random string has a violated edge. Either the claimed answers fail the test, so every edge of the string is violated, or they pass and therefore differ from the proof at some read. (With no reads there would be no edges, so the test must read at least once.)

noncomputable def Complexity.MultiTest.witnessEdge {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] [Nonempty Q] (A : M.toGraph.Assignment) (x : E × BooleanAnalysis.Cube M.R) : Fin (Fintype.card M.Edge)

A violated edge chosen for each rejecting string.

Equations

• M.witnessEdge A x = if h : x.2 ∈ M.rejects (M.tableOf A) x.1 then M.edgeIdx (x.1, x.2, Classical.choose ⋯) else M.edgeIdx (x.1, x.2, Classical.arbitrary Q)

theorem Complexity.MultiTest.witnessEdge_mem {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] [Nonempty Q] (A : M.toGraph.Assignment) (x : E × BooleanAnalysis.Cube M.R) (hx : x.2 ∈ M.rejects (M.tableOf A) x.1) : M.witnessEdge A x ∈ M.toGraph.unsatEdges A

theorem Complexity.MultiTest.witnessEdge_injective {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] [Nonempty Q] (A : M.toGraph.Assignment) : Function.Injective (M.witnessEdge A)

def Complexity.MultiTest.rejectPairs {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype E] (T : Table Pos) : Finset (E × BooleanAnalysis.Cube M.R)

The set of rejecting (test, random string) pairs.

Equations

• M.rejectPairs T = {x : E × Complexity.BooleanAnalysis.Cube M.R | x.2 ∈ M.rejects T x.1}

theorem Complexity.MultiTest.card_rejectPairs {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype E] (T : Table Pos) : (M.rejectPairs T).card = ∑ e : E, (M.rejects T e).card

theorem Complexity.MultiTest.card_rejects_le_card_unsatEdges {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] [Nonempty Q] (A : M.toGraph.Assignment) : ∑ e : E, (M.rejects (M.tableOf A) e).card ≤ (M.toGraph.unsatEdges A).card

Rejections are counted by violated edges.

theorem Complexity.MultiTest.numEdges_toGraph {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] : M.toGraph.numEdges = Fintype.card E * 2 ^ M.R * Fintype.card Q

theorem Complexity.MultiTest.unsatFrac_toGraph_ge {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] [Nonempty Q] (A : M.toGraph.Assignment) : (∑ e : E, ↑(M.rejects (M.tableOf A) e).card) / (↑(Fintype.card E) * 2 ^ M.R * ↑(Fintype.card Q)) ≤ M.toGraph.unsatFrac A

Soundness of the transformation. The violated fraction of the binary graph is at least the average rejection probability of the tests, divided by the number of reads.

Completeness

noncomputable def Complexity.MultiTest.honest {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (T : Table Pos) : M.toGraph.Assignment

The honest assignment: positions carry the proof, test vertices carry the answers the proof gives.

Equations

• M.honest T v = match (Complexity.NumEnc.equivFinCard M.Vert).symm v with | Sum.inl p => (T p, fun (x : Q) => 0) | Sum.inr (e, z) => (0, fun (i : Q) => T (M.pos e z i))

theorem Complexity.MultiTest.honest_inl {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (T : Table Pos) (p : Pos) : M.honest T (M.vertIdx (Sum.inl p)) = (T p, fun (x : Q) => 0)

theorem Complexity.MultiTest.honest_inr {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (T : Table Pos) (x : E × BooleanAnalysis.Cube M.R) : M.honest T (M.vertIdx (Sum.inr x)) = (0, fun (i : Q) => T (M.pos x.1 x.2 i))

theorem Complexity.MultiTest.satisfiable_toGraph {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] (T : Table Pos) (h : ∀ (e : E) (z : BooleanAnalysis.Cube M.R), M.accepts T e z = true) : M.toGraph.Satisfiable

Completeness. A proof accepted by every test on every random string gives a satisfying assignment of the binary graph.

theorem Complexity.MultiTest.prob_accepts_eq {Pos E Q : Type} (M : MultiTest Pos E Q) (T : Table Pos) (e : E) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube M.R) => M.accepts T e z = true) = 1 - ↑(M.rejects T e).card / 2 ^ M.R

The acceptance probability of a test, as a count of rejections.