Testing quadratic equations with the Hadamard code

A system of quadratic equations over the two-element field in the unknowns x : ι → Bool can be written as ⟨x ⊗ x, A e⟩ = b e for e : κ, where x ⊗ x : ι × ι → Bool is the tensor product of x with itself (BitString.tensor, the outer product Matrix.vecMulVec x x read on pairs of coordinates), and ⟨·, ·⟩ is the inner product modulo two, the dot product in the Boolean ring Bool. Bit strings add coordinatewise in the same ring, and the tensor product is bilinear (BitString.tensor_add_left, BitString.tensor_add_right). A proof that the system has a solution x consists of two tables: the Hadamard encodings f of x and g of x ⊗ x. Since ⟨x ⊗ x, y ⊗ z⟩ = ⟨x, y⟩ ⟨x, z⟩ (BitString.hadamardCode_tensor_tensor), the tables can be checked with a constant number of queries, every value being read by self-correction Arora and Barak, Section 11.5:

• the linearity test on f and on g (BitString.blrAcceptance): passing it, a table is close to the encoding of some bit string;
• the tensor test (BitString.tensorTestAcceptance), comparing g at y ⊗ z with the product of f at y and at z for uniformly random y and z: when g encodes w ≠ x ⊗ x, the encodings disagree on at least a quarter of the pairs (BitString.one_div_four_le_expect_hadamardCode_tensor), so the test rejects with probability at least 1/4 less the probability that a read is wrong (BitString.eq_tensor_of_lt_tensorTestAcceptance);
• the equation test (BitString.equationTestAcceptance), comparing g at the sum of a uniformly random set of the A e with the sum of the corresponding b e: when g encodes some w violating an equation, a random set of equations has a violated sum with probability one half (BitString.hadamardCode_eq_of_lt_equationTestAcceptance).

Together they make the Hadamard tester: the encodings of a solution pass all four tests with probability one, and tables passing them with high enough probability certify that the system is solvable, by a solution that f encodes (BitString.exists_forall_hadamardCode_tensor_eq_of_le_blrAcceptance).

Main definitions

• Cslib.BitString.tensor: the tensor product of two bit strings.
• Cslib.BitString.tensorTestAcceptance: the acceptance probability of the tensor test.
• Cslib.BitString.equationTestAcceptance: the acceptance probability of the equation test.

Main results

• Cslib.BitString.hadamardCode_tensor_tensor: the inner product of tensor products is the product of the inner products.
• Cslib.BitString.one_div_four_le_expect_hadamardCode_tensor: a nonzero bilinear form is nonzero on at least a quarter of the pairs.
• Cslib.BitString.tensorTestAcceptance_hadamardCode, Cslib.BitString.eq_tensor_of_lt_tensorTestAcceptance: completeness and soundness of the tensor test.
• Cslib.BitString.equationTestAcceptance_hadamardCode, Cslib.BitString.hadamardCode_eq_of_lt_equationTestAcceptance: completeness and soundness of the equation test.
• Cslib.BitString.exists_forall_hadamardCode_tensor_eq_of_le_blrAcceptance: soundness of the Hadamard tester for quadratic equations.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Tensor products

def Cslib.BitString.tensor {ι : Type u_1} {κ : Type u_2} (x : ι → Bool) (y : κ → Bool) : ι × κ → Bool

The tensor product of bit strings x and y: the outer product Matrix.vecMulVec x y in the Boolean ring Bool, read on pairs of coordinates, so its bit at (i, j) is x i && y j.

@[simp]

theorem Cslib.BitString.tensor_apply {ι : Type u_1} {κ : Type u_2} (x : ι → Bool) (y : κ → Bool) (p : ι × κ) : tensor x y p = (x p.1 && y p.2)

The bit of x ⊗ y at (i, j) is x i && y j.

theorem Cslib.BitString.tensor_add_left {ι : Type u_1} {κ : Type u_2} (x x' : ι → Bool) (y : κ → Bool) : tensor (x + x') y = tensor x y + tensor x' y

The tensor product is linear in its first argument.

theorem Cslib.BitString.tensor_add_right {ι : Type u_1} {κ : Type u_2} (x : ι → Bool) (y y' : κ → Bool) : tensor x (y + y') = tensor x y + tensor x y'

The tensor product is linear in its second argument.

theorem Cslib.BitString.tensor_single {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (i : ι) (j : κ) : tensor (Pi.single i true) (Pi.single j true) = Pi.single (i, j) true

The tensor product of two unit vectors is a unit vector.

theorem Cslib.BitString.hadamardCode_tensor_tensor {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (x a : ι → Bool) (y b : κ → Bool) : hadamardCode (tensor x y) (tensor a b) = (hadamardCode x a && hadamardCode y b)

The inner product of tensor products is the product of the inner products: ⟨x ⊗ y, a ⊗ b⟩ = ⟨x, a⟩ ⟨y, b⟩.

theorem Cslib.BitString.hadamardCode_tensor_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : ι → Bool) (p p' : ι) : hadamardCode (tensor x x) (Pi.single (p, p') true) = (x p && x p')

The Hadamard encoding of the tensor square of x, read at a unit vector, is a product of two bits of x.

theorem Cslib.BitString.one_div_four_le_expect_hadamardCode_tensor {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {M : ι × κ → Bool} (hM : ∃ (k : ι × κ), M k = true) : 1 / 4 ≤ Finset.univ.expect fun (y : ι → Bool) => Finset.univ.expect fun (z : κ → Bool) => if hadamardCode M (tensor y z) = true then 1 else 0

A nonzero bilinear form is nonzero on a quarter of the pairs: if M is not all false, then ⟨M, y ⊗ z⟩ = 1 with probability at least 1/4 over uniformly random y and z.

Union bounds

The tensor test

noncomputable def Cslib.BitString.tensorTestAcceptance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (g : (ι × ι → Bool) → Bool) : ℝ

The acceptance probability of the tensor test on tables f and g: the probability, over independent uniformly random y, z, r, s and t, that the self-corrected read of g at y ⊗ z with randomness t is the product of the self-corrected reads of f at y with randomness r and at z with randomness s.

@[simp]

theorem Cslib.BitString.tensorTestAcceptance_hadamardCode {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : ι → Bool) : tensorTestAcceptance (hadamardCode x) (hadamardCode (tensor x x)) = 1

Completeness of the tensor test: the encodings of x and of x ⊗ x pass it with probability one.

theorem Cslib.BitString.eq_tensor_of_lt_tensorTestAcceptance {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → Bool} {g : (ι × ι → Bool) → Bool} {x : ι → Bool} {w : ι × ι → Bool} {ε ε' : ℝ} (hf : ↑(hammingDist f (hadamardCode x)) / 2 ^ Fintype.card ι ≤ ε) (hg : ↑(hammingDist g (hadamardCode w)) / 2 ^ Fintype.card (ι × ι) ≤ ε') (h : 3 / 4 + (4 * ε + 2 * ε') < tensorTestAcceptance f g) : w = tensor x x

Soundness of the tensor test: if f and g are within relative distances ε and ε' of the encodings of x and of w, and the test accepts with probability more than 3/4 + 4ε + 2ε', then w = x ⊗ x.

The equation test

noncomputable def Cslib.BitString.equationTestAcceptance {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (g : (ι → Bool) → Bool) (A : κ → ι → Bool) (b : κ → Bool) : ℝ

The acceptance probability of the equation test on a table g, for the linear equations ⟨w, A e⟩ = b e in w: the probability, over independent uniformly random k and t, that the self-corrected read of g at the sum of the A e for the e with k e = true, with randomness t, is the sum of the corresponding b e.

theorem Cslib.BitString.equationTestAcceptance_hadamardCode {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {A : κ → ι → Bool} {b : κ → Bool} {w : ι → Bool} (h : ∀ (e : κ), hadamardCode w (A e) = b e) : equationTestAcceptance (hadamardCode w) A b = 1

Completeness of the equation test: the encoding of a solution of the equations passes it with probability one.

theorem Cslib.BitString.hadamardCode_eq_of_lt_equationTestAcceptance {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {g : (ι → Bool) → Bool} {A : κ → ι → Bool} {b : κ → Bool} {w : ι → Bool} {ε : ℝ} (hg : ↑(hammingDist g (hadamardCode w)) / 2 ^ Fintype.card ι ≤ ε) (h : 1 / 2 + 2 * ε < equationTestAcceptance g A b) (e : κ) : hadamardCode w (A e) = b e

Soundness of the equation test: if g is within relative distance ε of the encoding of w, and the test accepts with probability more than 1/2 + 2ε, then w solves the equations.

The Hadamard tester

theorem Cslib.BitString.exists_forall_hadamardCode_tensor_eq_of_le_blrAcceptance {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {f : (ι → Bool) → Bool} {g : (ι × ι → Bool) → Bool} {A : κ → ι × ι → Bool} {b : κ → Bool} {ε ε' : ℝ} (hf : 1 - ε ≤ blrAcceptance f) (hg : 1 - ε' ≤ blrAcceptance g) (htensor : 3 / 4 + (4 * ε + 2 * ε') < tensorTestAcceptance f g) (hequation : 1 / 2 + 2 * ε' < equationTestAcceptance g A b) : ∃ (x : ι → Bool), ↑(hammingDist f (hadamardCode x)) / 2 ^ Fintype.card ι ≤ ε ∧ ∀ (e : κ), hadamardCode (tensor x x) (A e) = b e

Soundness of the Hadamard tester for quadratic equations: if tables f and g pass the linearity test with probabilities at least 1 - ε and 1 - ε', the tensor test with probability more than 3/4 + 4ε + 2ε', and the equation test for A and b with probability more than 1/2 + 2ε', then f is within relative distance ε of the encoding of a solution x of the quadratic equations ⟨x ⊗ x, A e⟩ = b e.