The tester reads its input

An assignment tester is not a stand-alone proof system: it is given an input assignment — in Dinur's composition, the bits the outer constraint graph has already committed to at the two endpoints of an edge — and must reject unless those very bits extend to a satisfying assignment. A tester that merely certifies some satisfying assignment exists is useless there, because the outer graph's assignment would be free to disagree with it.

So the tester needs one more check: that the assignment a decoded from its proof agrees, on the input coordinates, with the input w it is handed. The check is the natural one — pick a random subset of the input coordinates, add up those bits of w directly (the input is a constant number of bits, so this costs nothing), and compare with the same subset-sum read off the proof by self-correction.

Soundness is the same rigidity argument that runs throughout the Hadamard analysis: two assignments whose subset-sums agree on more than half of the subsets are equal, because their difference would otherwise be a nonzero vector, and a nonzero vector's subset-sums are odd exactly half the time (prob_hadamard_ne_zero).

Main definitions

• Complexity.embedInput — an input string as a point of the full cube
• Complexity.InputAccepts — the input-consistency check on the raw table

Main results

• Complexity.eq_of_prob_hadamard_eq — rigidity: agreeing on more than half the subset-sums forces equality
• Complexity.eq_input_of_prob_inputAccepts — the tester verifies its input: passing the check often enough forces the decoded assignment to agree with the input
• Complexity.inputAccepts_of_honest — and the honest proof always passes
• Complexity.exists_sat_extending — the Hadamard code is an assignment tester: all four checks passing forces the input to extend to a satisfying assignment

Reading the input coordinates

def Complexity.embedInput {k t : ℕ} (r : BooleanAnalysis.Cube k) : BooleanAnalysis.Cube (k + t)

An input string, viewed as a point of the full cube: the input coordinates carry it and the auxiliary coordinates are zero. Reading a Hadamard table here returns a subset-sum of the input coordinates alone.

Equations

• Complexity.embedInput r = Fin.append r 0

theorem Complexity.hadamard_embedInput {k t : ℕ} (a : BooleanAnalysis.Cube (k + t)) (r : BooleanAnalysis.Cube k) : hadamard a (embedInput r) = hadamard (leftBlock a) r

Reading only the input coordinates. A subset-sum of an assignment taken at an embedded input string sees exactly the assignment's input part.

Rigidity

theorem Complexity.eq_of_prob_hadamard_eq {m : ℕ} (u v : BooleanAnalysis.Cube m) (h : 1 / 2 < BooleanAnalysis.prob fun (r : BooleanAnalysis.Cube m) => hadamard u r = hadamard v r) : u = v

Subset-sums determine an assignment. If two assignments' subset-sums agree on more than half of the subsets they are equal: otherwise their difference is a nonzero vector, whose subset-sums are odd on exactly half.

The input-consistency check

def Complexity.InputAccepts {k t : ℕ} (f : BooleanAnalysis.BooleanFunction (k + t)) (w : BooleanAnalysis.Cube k) (z : BooleanAnalysis.Cube (k + (k + t))) : Prop

The tester's input check, made on the raw table: a random subset-sum of the input, computed directly from the input bits, must equal the same subset-sum read off the proof by self-correction. The first block picks the subset, the second is the correction string.

Equations

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

theorem Complexity.prob_input_reads {k t : ℕ} (a : BooleanAnalysis.Cube (k + t)) (f : BooleanAnalysis.BooleanFunction (k + t)) (hf : BooleanAnalysis.IsBooleanValued f) {ε : ℝ} (hfc : BooleanAnalysis.IsClose f (signOf (hadamard a)) ε) : 1 - 2 * ε ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (k + (k + t))) => f (rightBlock z) * f (embedInput (leftBlock z) + rightBlock z) = BooleanAnalysis.chi (hadamard a (embedInput (leftBlock z)))

Every read of the input check is right except with probability 2ε. The subset is chosen by the first block and the correction by the second, so prob_blocks_ge fixes the read point before the correction is drawn.

theorem Complexity.eq_input_of_prob_inputAccepts {k t : ℕ} (a : BooleanAnalysis.Cube (k + t)) (w : BooleanAnalysis.Cube k) (f : BooleanAnalysis.BooleanFunction (k + t)) (hf : BooleanAnalysis.IsBooleanValued f) {ε : ℝ} (hfc : BooleanAnalysis.IsClose f (signOf (hadamard a)) ε) (haccept : 1 / 2 + 2 * ε < BooleanAnalysis.prob (InputAccepts f w)) : leftBlock a = w

The tester verifies its input. If the input check passes on more than half the randomness — with room for the reads' failure probability — then the assignment decoded from the proof agrees with the input on every input coordinate.

Together with exists_sat_of_prob_tester this is the assignment-tester guarantee Dinur's composition consumes: the proof cannot certify a satisfying assignment other than an extension of the bits the outer graph committed to.

theorem Complexity.inputAccepts_of_honest {k t : ℕ} (a : BooleanAnalysis.Cube (k + t)) (z : BooleanAnalysis.Cube (k + (k + t))) : InputAccepts (signOf (hadamard a)) (leftBlock a) z

Completeness of the input check. The honest proof for an assignment extending the input passes on every random string.

theorem Complexity.prob_inputAccepts_of_honest {k t : ℕ} (a : BooleanAnalysis.Cube (k + t)) : BooleanAnalysis.prob (InputAccepts (signOf (hadamard a)) (leftBlock a)) = 1

The honest proof passes the input check with probability one.

The assignment tester

theorem Complexity.exists_sat_extending {k t : ℕ} (C : QuadConstraint (k + t)) (w : BooleanAnalysis.Cube k) (f : BooleanAnalysis.BooleanFunction (k + t)) (hf : BooleanAnalysis.IsBooleanValued f) (g : BooleanAnalysis.BooleanFunction ((k + t) * (k + t))) (hg : BooleanAnalysis.IsBooleanValued g) {ε ε' : ℝ} (hblrf : BooleanAnalysis.blrAcceptProb f ≥ 1 - ε) (hblrg : BooleanAnalysis.blrAcceptProb g ≥ 1 - ε') (hcons : 3 / 4 + (4 * ε + 2 * ε') < BooleanAnalysis.prob (TesterAccepts f g)) (hchk : 2 * ε + 2 * ε' < BooleanAnalysis.prob (ConstraintAccepts f g C)) (hinp : 1 / 2 + 2 * ε < BooleanAnalysis.prob (InputAccepts f w)) : ∃ (a : BooleanAnalysis.Cube (k + t)), C.Sat a ∧ leftBlock a = w

The Hadamard code is an assignment tester. Given an input w and a proof consisting of two tables, if all four checks — linearity of each table, consistency of the quadratic table with the linear one, the constraint itself, and agreement with the input — pass often enough, then the input extends to a satisfying assignment of the constraint.

Nothing is assumed about the tables. This is the whole guarantee Dinur's alphabet-reduction step asks of its inner verifier: completeness is prob_testerAccepts_of_honest together with prob_inputAccepts_of_honest, and the query count and proof length depend only on the constraint's size, not on the outer system's.