Arithmetizing a constraint

The Hadamard tester checks a single quadratic equation over 𝔽₂. The constraint it is composed with in Dinur's proof is an arbitrary predicate on a constant number of bits — the relation of an outer edge, spelled out on the encodings of the two labels. Two gaps to close, both classical:

• An arbitrary predicate is not one quadratic equation, but it is a system of them once auxiliary variables are allowed. The system used here is the one-hot encoding: a selector variable for each candidate assignment, constrained to have exactly one selector set (a linear equation for the sum and a quadratic one for each pair), only selectors of satisfying candidates allowed, and the input bits equal to the selected candidate.

• A system of equations is checked with one query by taking a random linear combination: if any equation fails, the combination fails on exactly half of the coefficient vectors, because the failing values form a nonzero vector and a nonzero vector has odd inner product with half of all vectors.

Main definitions

• Complexity.QuadConstraint.combine — a linear combination of constraints
• Complexity.oneHotSystem — the one-hot system for a set of satisfying assignments

Main results

• Complexity.checkValue_combine — the check of a combination is the combination of the checks
• Complexity.forall_checkValue_of_prob — a combination passing on more than half the coefficient vectors means every equation passes
• Complexity.exists_sat_oneHotSystem, Complexity.mem_of_sat_oneHotSystem — the one-hot system is satisfiable exactly on the given set

Linearity of the Hadamard table

theorem Complexity.hadamard_add_arg {n : ℕ} (a x y : BooleanAnalysis.Cube n) : hadamard a (x + y) = hadamard a x + hadamard a y

Reading a Hadamard table at a sum of vectors.

theorem Complexity.hadamard_smul_arg {n : ℕ} (a : BooleanAnalysis.Cube n) (c : ZMod 2) (x : BooleanAnalysis.Cube n) : (hadamard a fun (i : Fin n) => c * x i) = c * hadamard a x

Reading a Hadamard table at a scalar multiple.

theorem Complexity.hadamard_sum_smul {n J : ℕ} (a : BooleanAnalysis.Cube n) (c : BooleanAnalysis.Cube J) (v : Fin J → BooleanAnalysis.Cube n) : (hadamard a fun (i : Fin n) => ∑ j : Fin J, c j * v j i) = ∑ j : Fin J, c j * hadamard a (v j)

Reading a Hadamard table at a finite sum of scaled vectors.

Random linear combinations

def Complexity.QuadConstraint.combine {n J : ℕ} (C : Fin J → QuadConstraint n) (c : BooleanAnalysis.Cube J) : QuadConstraint n

A linear combination of constraints with coefficients c.

Equations

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

theorem Complexity.checkValue_combine {n J : ℕ} (a : BooleanAnalysis.Cube n) (b : BooleanAnalysis.Cube (n * n)) (C : Fin J → QuadConstraint n) (c : BooleanAnalysis.Cube J) : checkValue (hadamard b) (hadamard a) (QuadConstraint.combine C c) = hadamard (fun (j : Fin J) => checkValue (hadamard b) (hadamard a) (C j)) c

The check of a combination is the combination of the checks, when the tables are Hadamard codewords (so linear).

theorem Complexity.forall_checkValue_of_prob {n J : ℕ} (a : BooleanAnalysis.Cube n) (b : BooleanAnalysis.Cube (n * n)) (C : Fin J → QuadConstraint n) (h : 1 / 2 < BooleanAnalysis.prob fun (c : BooleanAnalysis.Cube J) => checkValue (hadamard b) (hadamard a) (QuadConstraint.combine C c) = 0) (j : Fin J) : checkValue (hadamard b) (hadamard a) (C j) = 0

Rigidity of the combination. If the combined check passes on more than half of the coefficient vectors, every constraint's check passes.

theorem Complexity.QuadConstraint.sat_combine {n J : ℕ} (C : Fin J → QuadConstraint n) (a : BooleanAnalysis.Cube n) (h : ∀ (j : Fin J), (C j).Sat a) (c : BooleanAnalysis.Cube J) : (combine C c).Sat a

The combination of constraints satisfied by a is satisfied by a.

Reading a table at an appended vector

theorem Complexity.hadamard_append {k t : ℕ} (a : BooleanAnalysis.Cube (k + t)) (u : BooleanAnalysis.Cube k) (v : BooleanAnalysis.Cube t) : hadamard a (Fin.append u v) = hadamard (leftBlock a) u + hadamard (rightBlock a) v

Reading at an appended vector reads the two blocks separately.

theorem Complexity.hadamard_zero_arg {n : ℕ} (a : BooleanAnalysis.Cube n) : hadamard a 0 = 0

theorem Complexity.hadamard_tensorAssign_basisVec {n : ℕ} (a : BooleanAnalysis.Cube n) (u v : Fin n) : hadamard (tensorAssign a) (basisVec (finProdFinEquiv (u, v))) = a u * a v

The one-hot system

noncomputable def Complexity.candIdx (k : ℕ) : BooleanAnalysis.Cube k ≃ Fin (2 ^ k)

Candidate assignments, numbered.

Equations

• Complexity.candIdx k = Fintype.equivFinOfCardEq ⋯

def Complexity.auxVar (k : ℕ) (m : Fin (2 ^ k)) : Fin (k + 2 ^ k)

The selector variable of candidate number m.

Equations

• Complexity.auxVar k m = Fin.natAdd k m

def Complexity.QuadConstraint.trivial (n : ℕ) : QuadConstraint n

The trivial constraint 0 = 0.

Equations

• Complexity.QuadConstraint.trivial n = { quad := 0, lin := 0, const := 0 }

theorem Complexity.QuadConstraint.sat_trivial {n : ℕ} (a : BooleanAnalysis.Cube n) : (trivial n).Sat a

@[reducible, inline]

abbrev Complexity.OneHotIdx (k : ℕ) : Type

The index set of the one-hot system: the sum constraint, a constraint per pair of candidates, a constraint per candidate, and a constraint per input coordinate.

Equations

• Complexity.OneHotIdx k = (Unit ⊕ Fin (2 ^ k) × Fin (2 ^ k) ⊕ Fin (2 ^ k) ⊕ Fin k)

noncomputable def Complexity.oneHotOf {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) : OneHotIdx k → QuadConstraint (k + 2 ^ k)

The constraints of the one-hot system for the satisfying set S.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.oneHotOf S (Sum.inl PUnit.unit) = { quad := 0, lin := Fin.append 0 fun (x : Fin (2 ^ k)) => 1, const := 1 }
• Complexity.oneHotOf S (Sum.inr (Sum.inr (Sum.inr i))) = { quad := 0, lin := Fin.append (Complexity.basisVec i) fun (m : Fin (2 ^ k)) => (Complexity.candIdx k).symm m i, const := 0 }

noncomputable def Complexity.oneHotSystem {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) : Fin (Fintype.card (OneHotIdx k)) → QuadConstraint (k + 2 ^ k)

The one-hot system, as a Fin-indexed family for combine.

Equations

• Complexity.oneHotSystem S j = Complexity.oneHotOf S ((Fintype.equivFin (Complexity.OneHotIdx k)).symm j)

theorem Complexity.forall_oneHotSystem_iff {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (a : BooleanAnalysis.Cube (k + 2 ^ k)) : (∀ (j : Fin (Fintype.card (OneHotIdx k))), (oneHotSystem S j).Sat a) ↔ ∀ (x : OneHotIdx k), (oneHotOf S x).Sat a

Evaluating the constraints

theorem Complexity.sat_oneHot_sum_iff {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (a : BooleanAnalysis.Cube (k + 2 ^ k)) : (oneHotOf S (Sum.inl ())).Sat a ↔ ∑ m : Fin (2 ^ k), rightBlock a m = 1

theorem Complexity.sat_oneHot_pair_iff {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (a : BooleanAnalysis.Cube (k + 2 ^ k)) (m m' : Fin (2 ^ k)) (hne : m ≠ m') : (oneHotOf S (Sum.inr (Sum.inl (m, m')))).Sat a ↔ rightBlock a m * rightBlock a m' = 0

theorem Complexity.sat_oneHot_allowed_iff {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (a : BooleanAnalysis.Cube (k + 2 ^ k)) (m : Fin (2 ^ k)) (hm : (candIdx k).symm m ∉ S) : (oneHotOf S (Sum.inr (Sum.inr (Sum.inl m)))).Sat a ↔ rightBlock a m = 0

theorem Complexity.sat_oneHot_coord_iff {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (a : BooleanAnalysis.Cube (k + 2 ^ k)) (i : Fin k) : (oneHotOf S (Sum.inr (Sum.inr (Sum.inr i)))).Sat a ↔ leftBlock a i + ∑ m : Fin (2 ^ k), rightBlock a m * (candIdx k).symm m i = 0

Exactly one selector

theorem Complexity.eq_basis_of_sum_one {T : ℕ} (y : Fin T → ZMod 2) (hsum : ∑ m : Fin T, y m = 1) (hpair : ∀ (m m' : Fin T), m ≠ m' → y m * y m' = 0) : ∃ (m₀ : Fin T), y m₀ = 1 ∧ ∀ (m : Fin T), m ≠ m₀ → y m = 0

A 0/1 vector with odd sum and pairwise zero products is a basis vector.

The characterization

theorem Complexity.mem_of_sat_oneHotSystem {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (a : BooleanAnalysis.Cube (k + 2 ^ k)) (h : ∀ (j : Fin (Fintype.card (OneHotIdx k))), (oneHotSystem S j).Sat a) : leftBlock a ∈ S

Satisfying the one-hot system puts the input in the set.

noncomputable def Complexity.oneHotExtend {k : ℕ} (w : BooleanAnalysis.Cube k) : BooleanAnalysis.Cube (k + 2 ^ k)

The honest extension of an input: select its own candidate.

Equations

• Complexity.oneHotExtend w = Fin.append w fun (m : Fin (2 ^ k)) => if m = (Complexity.candIdx k) w then 1 else 0

theorem Complexity.leftBlock_oneHotExtend {k : ℕ} (w : BooleanAnalysis.Cube k) : leftBlock (oneHotExtend w) = w

theorem Complexity.rightBlock_oneHotExtend {k : ℕ} (w : BooleanAnalysis.Cube k) (m : Fin (2 ^ k)) : rightBlock (oneHotExtend w) m = if m = (candIdx k) w then 1 else 0

theorem Complexity.sat_oneHotSystem_extend {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (w : BooleanAnalysis.Cube k) (hw : w ∈ S) (j : Fin (Fintype.card (OneHotIdx k))) : (oneHotSystem S j).Sat (oneHotExtend w)

An input in the set satisfies the one-hot system, once extended by its own selector.

theorem Complexity.exists_sat_oneHotSystem_iff {k : ℕ} (S : Finset (BooleanAnalysis.Cube k)) (w : BooleanAnalysis.Cube k) : (∃ (a : BooleanAnalysis.Cube (k + 2 ^ k)), leftBlock a = w ∧ ∀ (j : Fin (Fintype.card (OneHotIdx k))), (oneHotSystem S j).Sat a) ↔ w ∈ S

The one-hot system is satisfiable exactly on the set.