The remaining checks of the assignment tester

HadamardTester proves the linearity and consistency checks. Two more are needed for the tester to plug into Dinur's composition, and both are analysed here on raw tables, over bundled randomness, in the same style.

• The constraint check on a system. The constraint is a system of quadratic equations (the one-hot arithmetization of Arithmetize), checked by one random linear combination. Passing on more than half of the coefficient vectors — after paying for the reads — forces every equation to hold on the decoded tables.

• The input check, one coordinate at a time. The tester is handed its input as a table it may read at a single random coordinate, and compares that bit with the corresponding coordinate of its decoded assignment, obtained by self-correction at a basis vector. Passing often means the input table is close to the decoded assignment's input part — not equal, which a single read could never certify, but close enough that, when the input is supposed to be a Hadamard codeword, it decodes uniquely.

The last point is what makes the composition work with constantly many queries: the outer graph's labels are handed to the tester as Hadamard codewords, and a wrong label is far from every right one.

Main results

• Complexity.forall_checkValue_of_prob_combined — the random-combination constraint check
• Complexity.prob_coord_eq_ge — the single-coordinate input check
• Complexity.decodeLabel_eq — a table close to a codeword decodes to it

The constraint check on a system

theorem Complexity.forall_checkValue_of_prob_combined {n J : ℕ} (a : BooleanAnalysis.Cube n) (b : BooleanAnalysis.Cube (n * n)) (C : Fin J → QuadConstraint n) (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) {ε : ℝ} (hfc : BooleanAnalysis.IsClose f (signOf (hadamard a)) ε) (g : BooleanAnalysis.BooleanFunction (n * n)) (hg : BooleanAnalysis.IsBooleanValued g) {ε' : ℝ} (hgc : BooleanAnalysis.IsClose g (signOf (hadamard b)) ε') (haccept : 1 / 2 + (2 * ε + 2 * ε') < BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (J + (n + n * n))) => ConstraintAccepts f g (QuadConstraint.combine C (leftBlock z)) (rightBlock z)) (j : Fin J) : checkValue (hadamard b) (hadamard a) (C j) = 0

The random-combination constraint check. Reading the combined constraint off the raw tables passes often enough only if every constraint of the system holds on the decoded tables. The coefficient vector is the first block, the correction strings the second.

The input check, one coordinate at a time

def Complexity.CoordAccepts {n m : ℕ} (f : BooleanAnalysis.BooleanFunction n) (w : BooleanAnalysis.Cube m → ZMod 2) (idx : BooleanAnalysis.Cube m → Fin n) (z : BooleanAnalysis.Cube (m + n)) : Prop

The single-coordinate input check, on the raw table: a random coordinate r (first block) of the input table w is compared with the decoded assignment's bit at variable idx r, read by self-correction at the basis vector (correction string: second block).

Equations

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

theorem Complexity.prob_coord_eq_ge {n m : ℕ} (a : BooleanAnalysis.Cube n) (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) {ε : ℝ} (hfc : BooleanAnalysis.IsClose f (signOf (hadamard a)) ε) (w : BooleanAnalysis.Cube m → ZMod 2) (idx : BooleanAnalysis.Cube m → Fin n) : BooleanAnalysis.prob (CoordAccepts f w idx) - 2 * ε ≤ BooleanAnalysis.prob fun (r : BooleanAnalysis.Cube m) => a (idx r) = w r

Passing the coordinate check means agreeing on most coordinates.

theorem Complexity.coordAccepts_of_honest {n m : ℕ} (a : BooleanAnalysis.Cube n) (idx : BooleanAnalysis.Cube m → Fin n) (z : BooleanAnalysis.Cube (m + n)) : CoordAccepts (signOf (hadamard a)) (fun (r : BooleanAnalysis.Cube m) => a (idx r)) idx z

The honest table passes the coordinate check everywhere, when the input table is the decoded assignment's input part.

Decoding a label from a table

noncomputable def Complexity.bitDist {m : ℕ} (s t : BooleanAnalysis.Cube m → ZMod 2) : ℝ

The distance between two bit tables: the fraction of coordinates where they differ.

Equations

• Complexity.bitDist s t = Complexity.BooleanAnalysis.prob fun (r : Complexity.BooleanAnalysis.Cube m) => s r ≠ t r

theorem Complexity.bitDist_eq_hammingDist {m : ℕ} (s t : BooleanAnalysis.Cube m → ZMod 2) : bitDist s t = BooleanAnalysis.hammingDist (signOf s) (signOf t)

theorem Complexity.bitDist_comm {m : ℕ} (s t : BooleanAnalysis.Cube m → ZMod 2) : bitDist s t = bitDist t s

theorem Complexity.bitDist_triangle {m : ℕ} (s t u : BooleanAnalysis.Cube m → ZMod 2) : bitDist s u ≤ bitDist s t + bitDist t u

theorem Complexity.bitDist_eq_one_sub {m : ℕ} (s t : BooleanAnalysis.Cube m → ZMod 2) : bitDist s t = 1 - BooleanAnalysis.prob fun (r : BooleanAnalysis.Cube m) => s r = t r

theorem Complexity.bitDist_hadamard {m : ℕ} (u v : BooleanAnalysis.Cube m) (h : u ≠ v) : bitDist (hadamard u) (hadamard v) = 1 / 2

Distinct codewords are far apart: at distance exactly one half.

noncomputable def Complexity.decodeLabel {m : ℕ} {β : Type} [Nonempty β] (enc : β → BooleanAnalysis.Cube m) (t : BooleanAnalysis.Cube m → ZMod 2) : β

Decoding: the label whose codeword is within a quarter of the table, if any; an arbitrary label otherwise.

Equations

• Complexity.decodeLabel enc t = if h : ∃ (σ : β), Complexity.bitDist t (Complexity.hadamard (enc σ)) < 1 / 4 then Classical.choose h else Classical.arbitrary β

theorem Complexity.decodeLabel_eq {m : ℕ} {β : Type} [Nonempty β] (enc : β → BooleanAnalysis.Cube m) (henc : Function.Injective enc) (t : BooleanAnalysis.Cube m → ZMod 2) (σ : β) (h : bitDist t (hadamard (enc σ)) < 1 / 4) : decodeLabel enc t = σ

A table close to a codeword decodes to its label.