The assignment tester, assembled

The six checks of the Hadamard assignment tester, run on one bundled random string, on raw tables, with a universal soundness constant.

The tester is handed two input tables Tt Th : Cube B → ZMod 2 — in the composition, the Hadamard encodings of the labels at the two ends of an outer edge — and a proof consisting of a linear table F over n variables and a quadratic table G over n * n, where the n variables are the 2 · 2^B input coordinates followed by the selectors of a one-hot system. Its random string has six blocks, one per check:

1. linearity of F; 2. linearity of G; 3. consistency of G with F;
2. the one-hot system, by a random linear combination; 5. and 6. the two input tables, one coordinate each.

Every check reads a constant number of positions — never a whole table — so the total query count is a constant independent of B, and the soundness constant 1/32 is universal. That independence is the point of the tester: the outer alphabet may be enormous, and neither the query count nor the soundness loss may notice.

Main definitions

• Complexity.Tester.AllChecks — the tester's verdict on a random string

Main results

• Complexity.Tester.sound — passing with probability above 31/32 yields an assignment satisfying the system whose input parts are within 3/32 of the input tables
• Complexity.Tester.complete — the honest proof of a satisfying assignment passes on every random string

Layout

@[reducible, inline]

abbrev Complexity.Tester.kOf (B : ℕ) : ℕ

The number of input variables: two tables of 2^B coordinates.

Equations

• Complexity.Tester.kOf B = 2 ^ B + 2 ^ B

@[reducible, inline]

abbrev Complexity.Tester.nOf (B : ℕ) : ℕ

The number of variables: input coordinates and one-hot selectors.

Equations

• Complexity.Tester.nOf B = Complexity.Tester.kOf B + 2 ^ Complexity.Tester.kOf B

@[reducible, inline]

abbrev Complexity.Tester.JOf (B : ℕ) : ℕ

The number of constraints in the one-hot system.

Equations

• Complexity.Tester.JOf B = Fintype.card (Complexity.OneHotIdx (Complexity.Tester.kOf B))

noncomputable def Complexity.Tester.inTail (B : ℕ) (r : BooleanAnalysis.Cube B) : Fin (nOf B)

The variable holding coordinate r of the first input table.

Equations

• Complexity.Tester.inTail B r = Fin.castAdd (2 ^ Complexity.Tester.kOf B) (Fin.castAdd (2 ^ B) ((Complexity.candIdx B) r))

noncomputable def Complexity.Tester.inHead (B : ℕ) (r : BooleanAnalysis.Cube B) : Fin (nOf B)

The variable holding coordinate r of the second input table.

Equations

• Complexity.Tester.inHead B r = Fin.castAdd (2 ^ Complexity.Tester.kOf B) (Fin.natAdd (2 ^ B) ((Complexity.candIdx B) r))

noncomputable def Complexity.Tester.tailPart {B : ℕ} (a : BooleanAnalysis.Cube (nOf B)) : BooleanAnalysis.Cube B → ZMod 2

The first input table an assignment of the variables carries.

Equations

• Complexity.Tester.tailPart a r = a (Complexity.Tester.inTail B r)

noncomputable def Complexity.Tester.headPart {B : ℕ} (a : BooleanAnalysis.Cube (nOf B)) : BooleanAnalysis.Cube B → ZMod 2

The second input table an assignment of the variables carries.

Equations

• Complexity.Tester.headPart a r = a (Complexity.Tester.inHead B r)

@[reducible, inline]

abbrev Complexity.Tester.R1 (B : ℕ) : ℕ

The random bits of the linearity check on F.

Equations

• Complexity.Tester.R1 B = Complexity.Tester.nOf B + Complexity.Tester.nOf B

@[reducible, inline]

abbrev Complexity.Tester.R2 (B : ℕ) : ℕ

The random bits of the linearity check on G.

Equations

• Complexity.Tester.R2 B = Complexity.Tester.nOf B * Complexity.Tester.nOf B + Complexity.Tester.nOf B * Complexity.Tester.nOf B

@[reducible, inline]

abbrev Complexity.Tester.R3 (B : ℕ) : ℕ

The random bits of the consistency check.

Equations

• Complexity.Tester.R3 B = Complexity.Tester.nOf B + Complexity.Tester.nOf B + (Complexity.Tester.nOf B + (Complexity.Tester.nOf B + Complexity.Tester.nOf B * Complexity.Tester.nOf B))

@[reducible, inline]

abbrev Complexity.Tester.R4 (B : ℕ) : ℕ

The random bits of the constraint check.

Equations

• Complexity.Tester.R4 B = Complexity.Tester.JOf B + (Complexity.Tester.nOf B + Complexity.Tester.nOf B * Complexity.Tester.nOf B)

@[reducible, inline]

abbrev Complexity.Tester.R5 (B : ℕ) : ℕ

The random bits of one input check.

Equations

• Complexity.Tester.R5 B = B + Complexity.Tester.nOf B

@[reducible, inline]

abbrev Complexity.Tester.Rest5 (B : ℕ) : ℕ

The random bits of the last two blocks.

Equations

• Complexity.Tester.Rest5 B = Complexity.Tester.R5 B + Complexity.Tester.R5 B

@[reducible, inline]

abbrev Complexity.Tester.Rest4 (B : ℕ) : ℕ

The random bits of the last three blocks.

Equations

• Complexity.Tester.Rest4 B = Complexity.Tester.R4 B + Complexity.Tester.Rest5 B

@[reducible, inline]

abbrev Complexity.Tester.Rest3 (B : ℕ) : ℕ

The random bits of the last four blocks.

Equations

• Complexity.Tester.Rest3 B = Complexity.Tester.R3 B + Complexity.Tester.Rest4 B

@[reducible, inline]

abbrev Complexity.Tester.Rest2 (B : ℕ) : ℕ

The random bits after the first block.

Equations

• Complexity.Tester.Rest2 B = Complexity.Tester.R2 B + Complexity.Tester.Rest3 B

@[reducible, inline]

abbrev Complexity.Tester.ROf (B : ℕ) : ℕ

The total number of random bits.

Equations

• Complexity.Tester.ROf B = Complexity.Tester.R1 B + Complexity.Tester.Rest2 B

def Complexity.Tester.blk1 {B : ℕ} (z : BooleanAnalysis.Cube (ROf B)) : BooleanAnalysis.Cube (R1 B)

The first block of the random string: linearity of F.

Equations

• Complexity.Tester.blk1 z = Complexity.leftBlock z

def Complexity.Tester.blk2 {B : ℕ} (z : BooleanAnalysis.Cube (ROf B)) : BooleanAnalysis.Cube (R2 B)

The second block: linearity of G.

Equations

• Complexity.Tester.blk2 z = Complexity.leftBlock (Complexity.rightBlock z)

def Complexity.Tester.blk3 {B : ℕ} (z : BooleanAnalysis.Cube (ROf B)) : BooleanAnalysis.Cube (R3 B)

The third block: consistency.

Equations

• Complexity.Tester.blk3 z = Complexity.leftBlock (Complexity.rightBlock (Complexity.rightBlock z))

def Complexity.Tester.blk4 {B : ℕ} (z : BooleanAnalysis.Cube (ROf B)) : BooleanAnalysis.Cube (R4 B)

The fourth block: the constraint system.

Equations

• Complexity.Tester.blk4 z = Complexity.leftBlock (Complexity.rightBlock (Complexity.rightBlock (Complexity.rightBlock z)))

def Complexity.Tester.blk5 {B : ℕ} (z : BooleanAnalysis.Cube (ROf B)) : BooleanAnalysis.Cube (R5 B)

The fifth block: the first input table.

Equations

• Complexity.Tester.blk5 z = Complexity.leftBlock (Complexity.rightBlock (Complexity.rightBlock (Complexity.rightBlock (Complexity.rightBlock z))))

def Complexity.Tester.blk6 {B : ℕ} (z : BooleanAnalysis.Cube (ROf B)) : BooleanAnalysis.Cube (R5 B)

The sixth block: the second input table.

Equations

• Complexity.Tester.blk6 z = Complexity.rightBlock (Complexity.rightBlock (Complexity.rightBlock (Complexity.rightBlock (Complexity.rightBlock z))))

Each block is uniform

theorem Complexity.Tester.prob_blk1 {B : ℕ} (P : BooleanAnalysis.Cube (R1 B) → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (ROf B)) => P (blk1 z)) = BooleanAnalysis.prob P

theorem Complexity.Tester.prob_blk2 {B : ℕ} (P : BooleanAnalysis.Cube (R2 B) → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (ROf B)) => P (blk2 z)) = BooleanAnalysis.prob P

theorem Complexity.Tester.prob_blk3 {B : ℕ} (P : BooleanAnalysis.Cube (R3 B) → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (ROf B)) => P (blk3 z)) = BooleanAnalysis.prob P

theorem Complexity.Tester.prob_blk4 {B : ℕ} (P : BooleanAnalysis.Cube (R4 B) → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (ROf B)) => P (blk4 z)) = BooleanAnalysis.prob P

theorem Complexity.Tester.prob_blk5 {B : ℕ} (P : BooleanAnalysis.Cube (R5 B) → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (ROf B)) => P (blk5 z)) = BooleanAnalysis.prob P

theorem Complexity.Tester.prob_blk6 {B : ℕ} (P : BooleanAnalysis.Cube (R5 B) → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (ROf B)) => P (blk6 z)) = BooleanAnalysis.prob P

The checks

def Complexity.Tester.LinCheck {m : ℕ} (f : BooleanAnalysis.BooleanFunction m) (x : BooleanAnalysis.Cube (m + m)) : Prop

The linearity check on a table, reading at the two halves of the block and their sum.

Equations

• Complexity.Tester.LinCheck f x = (f (Complexity.leftBlock x) * f (Complexity.rightBlock x) = f (Complexity.leftBlock x + Complexity.rightBlock x))

theorem Complexity.Tester.prob_linCheck {m : ℕ} (f : BooleanAnalysis.BooleanFunction m) : BooleanAnalysis.prob (LinCheck f) = BooleanAnalysis.blrAcceptProb f

def Complexity.Tester.AllChecks {B : ℕ} (S : Finset (BooleanAnalysis.Cube (kOf B))) (Tt Th : BooleanAnalysis.Cube B → ZMod 2) (F : BooleanAnalysis.Cube (nOf B) → ZMod 2) (G : BooleanAnalysis.Cube (nOf B * nOf B) → ZMod 2) (z : BooleanAnalysis.Cube (ROf B)) : Prop

The tester's verdict: all six checks pass on the random string.

Equations

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

theorem Complexity.Tester.isBooleanValued_signOf {m : ℕ} (F : BooleanAnalysis.Cube m → ZMod 2) : BooleanAnalysis.IsBooleanValued (signOf F)

Soundness

theorem Complexity.Tester.sound {B : ℕ} (S : Finset (BooleanAnalysis.Cube (kOf B))) (Tt Th : BooleanAnalysis.Cube B → ZMod 2) (F : BooleanAnalysis.Cube (nOf B) → ZMod 2) (G : BooleanAnalysis.Cube (nOf B * nOf B) → ZMod 2) (h : 1 - 1 / 32 < BooleanAnalysis.prob (AllChecks S Tt Th F G)) : ∃ (a : BooleanAnalysis.Cube (nOf B)), (∀ (j : Fin (Fintype.card (OneHotIdx (kOf B)))), (oneHotSystem S j).Sat a) ∧ bitDist Tt (tailPart a) ≤ 3 / 32 ∧ bitDist Th (headPart a) ≤ 3 / 32

Soundness of the assembled tester. If the six checks all pass with probability above 31/32, the proof decodes to an assignment of the variables that satisfies the one-hot system and whose two input parts are within 3/32 of the input tables.

Completeness

theorem Complexity.Tester.linCheck_hadamard {m : ℕ} (a : BooleanAnalysis.Cube m) (x : BooleanAnalysis.Cube (m + m)) : LinCheck (signOf (hadamard a)) x

theorem Complexity.Tester.constraintAccepts_of_honest {m : ℕ} (a : BooleanAnalysis.Cube m) (C : QuadConstraint m) (hC : C.Sat a) (z : BooleanAnalysis.Cube (m + m * m)) : ConstraintAccepts (signOf (hadamard a)) (signOf (hadamard (tensorAssign a))) C z

The honest tables pass the constraint check on every random string.

theorem Complexity.Tester.complete {B : ℕ} (S : Finset (BooleanAnalysis.Cube (kOf B))) (a : BooleanAnalysis.Cube (nOf B)) (ha : ∀ (j : Fin (Fintype.card (OneHotIdx (kOf B)))), (oneHotSystem S j).Sat a) (z : BooleanAnalysis.Cube (ROf B)) : AllChecks S (tailPart a) (headPart a) (hadamard a) (hadamard (tensorAssign a)) z

Completeness of the assembled tester. The honest proof of an assignment satisfying the system — its Hadamard encoding and that of its tensor square, with the input tables read off the assignment — passes every check on every random string.