One round, in numbers #

A round of amplification multiplies both counts of a constraint graph by a constant factor. This module records those factors, so an algorithm that writes the round's output knows how big it is.

Main results #

Complexity.MultiTest.numVerts_toGraph — the vertices of a family's graph
Complexity.RegCSP.card_pos_compose — the positions of a composed proof
Complexity.Dinur.numVerts_step — a round's vertex count
Complexity.MultiTest.tailNum_eq — the first endpoint of an edge
Complexity.MultiTest.rel_toGraph_eq — its constraint, from the verdict and the read

source

theorem Complexity.MultiTest.numVerts_toGraph {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype E] [Fintype Q] [NumEnc Pos] [NumEnc E] [NumEnc Q] :

M.toGraph.numVerts = Fintype.card Pos + Fintype.card E * 2 ^ M.R

The vertices: one per position, and one per (test, random string).

source

theorem Complexity.MultiTest.split_mixed {a b c C Q : ℕ} (hb : b < C) (hc : c < Q) :

(a * (C * Q) + (b * Q + c)) / (C * Q) = a ∧ (a * (C * Q) + (b * Q + c)) % (C * Q) / Q = b ∧ (a * (C * Q) + (b * Q + c)) % Q = c

Splitting a number into a quotient and a remainder, with the remainder itself split.

source

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

NumEnc.enc (M.edgeOf k).1 = ↑k / (2 ^ M.R * Fintype.card Q) ∧ NumEnc.enc (M.edgeOf k).2.1 = ↑k % (2 ^ M.R * Fintype.card Q) / Fintype.card Q ∧ NumEnc.enc (M.edgeOf k).2.2 = ↑k % Fintype.card Q

How an edge number splits: the test, the random string, the read.

source

noncomputable def Complexity.MultiTest.tailNum {Pos E Q : Type} (M : MultiTest Pos E Q) [Fintype Pos] [Fintype Q] (k : ℕ) :

ℕ

The first endpoint of an edge, in numbers.

Equations

M.tailNum k = Fintype.card Pos + (k / (2 ^ M.R * Fintype.card Q) * 2 ^ M.R + k % (2 ^ M.R * Fintype.card Q) / Fintype.card Q)

Instances For

source

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

M.tailNum ↑k = ↑(M.toGraph.tail k)

source

def Complexity.MultiTest.relOfCheck {Q : Type} (chk : (Q → ZMod 2) → Bool) (i : Q) :

Alpha Q → Alpha Q → Bool

The constraint an edge carries: the test vertex's answers must pass the test, and the read's answer must be the position's bit.

Equations

Complexity.MultiTest.relOfCheck chk i l₁ l₂ = decide (chk l₁.2 = true ∧ l₁.2 i = l₂.1)

Instances For

source

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

M.toGraph.rel k = relOfCheck (M.check (M.edgeOf k).1 (M.edgeOf k).2.1) (M.edgeOf k).2.2

The constraint depends only on the verdict and the read.

source

theorem Complexity.RegCSP.card_pos_compose {β : Type} (R : RegCSP β) (B : ℕ) :

Fintype.card R.Pos = R.graph.order * 2 ^ B + (R.graph.order * R.graph.deg * 2 ^ Tester.nOf B + R.graph.order * R.graph.deg * 2 ^ (Tester.nOf B * Tester.nOf B))

The positions of a composed proof: an encoding block per vertex, and a linear and a quadratic table per dart.

source

theorem Complexity.RegCSP.R_compose {β : Type} [Fintype β] (R : RegCSP β) (B : ℕ) (enc : β → BooleanAnalysis.Cube B) :

(compose enc R).R = Tester.ROf B

The composed test's randomness.

source

theorem Complexity.RegCSP.edge_split {β : Type} [Fintype β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (B : ℕ) (enc : β → BooleanAnalysis.Cube B) (k : Fin (Fintype.card (compose enc R).Edge)) :

↑k = ((NumEnc.enc ((compose enc R).edgeOf k).1.1 * NumEnc.card R.graph.D + NumEnc.enc ((compose enc R).edgeOf k).1.2) * 2 ^ Tester.ROf B + NumEnc.enc ((compose enc R).edgeOf k).2.1) * 22 + NumEnc.enc ((compose enc R).edgeOf k).2.2

An edge number splits into a vertex, a dart, a string and a read.

source

theorem Complexity.RegCSP.tailNum_split {β : Type} [Fintype β] (R : RegCSP β) (B : ℕ) (enc : β → BooleanAnalysis.Cube B) (a c d : ℕ) (hc : c < 2 ^ Tester.ROf B) (hd : d < 22) :

(compose enc R).tailNum ((a * 2 ^ Tester.ROf B + c) * 22 + d) = Fintype.card R.Pos + (a * 2 ^ Tester.ROf B + c)

The first endpoint, from an edge's split.

source

theorem Complexity.RegCSP.tailNum_split' {β : Type} [Fintype β] (R : RegCSP β) (B : ℕ) (enc : β → BooleanAnalysis.Cube B) (cZ a c d : ℕ) (hcZ : cZ = 2 ^ Tester.ROf B) (hc : c < cZ) (hd : d < 22) :

(compose enc R).tailNum ((a * cZ + c) * 22 + d) = Fintype.card R.Pos + (a * cZ + c)

The first endpoint, with the string count given by name.

source

theorem Complexity.RegCSP.edge_data {β : Type} [Fintype β] (R : RegCSP β) [NumEnc R.graph.V] [NumEnc R.graph.D] (B : ℕ) (enc : β → BooleanAnalysis.Cube B) (e : ℕ) (he : e < (compose enc R).toGraph.numEdges) :

∃ (p : R.Dart) (z : BooleanAnalysis.Cube (Tester.ROf B)) (i : ReadIdx), p = ((compose enc R).edgeOf ⟨e, he⟩).1 ∧ z = ((compose enc R).edgeOf ⟨e, he⟩).2.1 ∧ i = ((compose enc R).edgeOf ⟨e, he⟩).2.2 ∧ e = ((NumEnc.enc p.1 * NumEnc.card R.graph.D + NumEnc.enc p.2) * 2 ^ Tester.ROf B + NumEnc.enc z) * 22 + NumEnc.enc i

An edge's data, packaged so that a caller never has to spell the composed system out: the test, the string and the read it names, together with how its number splits.

source