Decoding a Hadamard proof

Dinur's alphabet-reduction step composes a constraint system with an inner verifier — an assignment tester — and the classical one is built from the Hadamard code: an assignment a ⊆ Fin n is encoded as the parity function χ a, and the verifier checks that the proof is (close to) such a function.

The two facts the analysis rests on are already in Complexitylib.BooleanAnalysis.FourierExpansion: blr_soundness, which says a proof passing the linearity test is close to some linear function, and local_correctability, which recovers that function's value anywhere. What is missing for a tester is the witness: soundness must hand back the coordinate set S, since S is precisely the assignment being decoded.

This module extracts that witness, and records the two identities that make χ S a usable decoding: its value on a basis vector is the membership bit of S, so reading the corrected proof at basis vectors recovers the assignment.

Main results

• Complexity.exists_close_parity_of_blr — soundness with the coordinate set named
• Complexity.parityFun_basis — the decoded assignment is read off at basis vectors
• Complexity.hadamard, Complexity.signOf_hadamard — the Hadamard code is a parity function, so the Fourier results apply to it
• Complexity.tensor, Complexity.hadamard_tensor — the consistency identity tying the quadratic table to the linear one
• Complexity.parity_eq_signOf_hadamard, Complexity.exists_assignment_of_blr — a proof passing the linearity test decodes to an assignment
• Complexity.eq_tensorAssign_of_consistent — the consistency check leaves the prover no freedom in the quadratic table
• Complexity.QuadConstraint, Complexity.sat_of_checks — the constraint check, and tester soundness in exact form
• Complexity.checks_of_sat — and its completeness
• Complexity.hammingDist_comm, Complexity.hammingDist_triangle — basic metric facts, absent from the Fourier layer
• Complexity.eq_of_hammingDist_lt_half, Complexity.hadamard_inj_of_close — the decoding is rigid, so a check passing often holds exactly
• Complexity.prob_hadamard_ne_zero — a nonzero linear form is balanced
• Complexity.tensorRow, Complexity.hadamard_tensor_row — the bilinear form, read as a linear form in one argument
• Complexity.prob_mono, Complexity.prob_tensorRow_ne_zero — a nonzero bilinear form has nonzero rows for at least half the second arguments
• Complexity.prob₂_tensor_ne_zero — hence it is nonzero on a quarter of all pairs
• Complexity.eq_tensorAssign_of_prob_consistent — so passing the consistency check often forces the quadratic table exactly
• Complexity.prob_corrected_read_left, Complexity.prob_two_corrected_reads — self-corrected reads over bundled randomness
• Complexity.sat_of_prob_checks — soundness when consistency is only tested on a random pair
• Complexity.prob_consistency_of_honest — and the matching completeness
• Complexity.prob_all_reads — every read of a tester is correct, for any bundling of its randomness

theorem Complexity.exists_close_parity_of_blr {n : ℕ} (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) (ε : ℝ) (h : BooleanAnalysis.blrAcceptProb f ≥ 1 - ε) : ∃ (S : Finset (Fin n)), BooleanAnalysis.hammingDist f (BooleanAnalysis.parityFun S) ≤ ε

BLR soundness, with the witness named. A proof passing the linearity test is close to χ S for an explicit coordinate set S — and S is the assignment the tester decodes.

def Complexity.basisVec {n : ℕ} (i : Fin n) : BooleanAnalysis.Cube n

The basis vector at coordinate i.

Equations

• Complexity.basisVec i j = if j = i then 1 else 0

theorem Complexity.parityFun_basis {n : ℕ} (S : Finset (Fin n)) (i : Fin n) : BooleanAnalysis.parityFun S (basisVec i) = if i ∈ S then -1 else 1

Reading the assignment. The decoded parity function, evaluated at the i-th basis vector, is -1 exactly when i belongs to the coordinate set: the assignment is read off the proof one coordinate at a time.

The Hadamard code

@[reducible, inline]

abbrev Complexity.BitFun (n : ℕ) : Type

An 𝔽₂-valued function on the cube. The tester's checks are stated over 𝔽₂ — the consistency check multiplies two bits, which is not a ±1 operation — while the linearity analysis lives in the ±1 world, so the two views must be bridged.

Equations

• Complexity.BitFun n = (Complexity.BooleanAnalysis.Cube n → ZMod 2)

noncomputable def Complexity.signOf {n : ℕ} (F : BitFun n) : BooleanAnalysis.BooleanFunction n

The ±1 encoding of an 𝔽₂-valued function.

Equations

• Complexity.signOf F x = Complexity.BooleanAnalysis.chi (F x)

theorem Complexity.chi_sum {ι : Type u_1} (s : Finset ι) (f : ι → ZMod 2) : BooleanAnalysis.chi (∑ i ∈ s, f i) = ∏ i ∈ s, BooleanAnalysis.chi (f i)

def Complexity.hadamard {n : ℕ} (a : BooleanAnalysis.Cube n) : BitFun n

The Hadamard encoding of an assignment a: the linear function x ↦ ⟨a, x⟩.

Equations

• Complexity.hadamard a x = ∑ i : Fin n, a i * x i

theorem Complexity.signOf_hadamard {n : ℕ} (a : BooleanAnalysis.Cube n) : signOf (hadamard a) = BooleanAnalysis.parityFun {i : Fin n | a i = 1}

The Hadamard code is a parity function. Its ±1 encoding is χ of the support of the assignment — so the Fourier layer's linearity results apply to Hadamard proofs verbatim, and the decoded coordinate set is the assignment's support.

The tensor part

def Complexity.tensor {n : ℕ} (x y : BooleanAnalysis.Cube n) : BooleanAnalysis.Cube (n * n)

The outer product of two cube points, as a point of the squared cube. The Fourier layer is indexed by Fin n, so the pair index is transported along finProdFinEquiv.

Equations

• Complexity.tensor x y k = x (finProdFinEquiv.symm k).1 * y (finProdFinEquiv.symm k).2

def Complexity.tensorAssign {n : ℕ} (a : BooleanAnalysis.Cube n) : BooleanAnalysis.Cube (n * n)

The tensor square of an assignment — the second table a Hadamard proof carries, so that the verifier can evaluate quadratic constraints.

Equations

• Complexity.tensorAssign a = Complexity.tensor a a

theorem Complexity.hadamard_tensor {n : ℕ} (a x y : BooleanAnalysis.Cube n) : hadamard (tensorAssign a) (tensor x y) = hadamard a x * hadamard a y

The consistency identity. The tensor table, read at an outer product, is the product of the two linear readings. This is the check that ties the quadratic table to the linear one, and it is a statement about bits: over 𝔽₂ the right-hand side is a product, which is why the tester's checks cannot be phrased in the ±1 encoding.

Decoding a proof into an assignment

def Complexity.indicatorAssign {n : ℕ} (S : Finset (Fin n)) : BooleanAnalysis.Cube n

The assignment a coordinate set stands for.

Equations

• Complexity.indicatorAssign S i = if i ∈ S then 1 else 0

theorem Complexity.parity_eq_signOf_hadamard {n : ℕ} (S : Finset (Fin n)) : BooleanAnalysis.parityFun S = signOf (hadamard (indicatorAssign S))

Every parity function is a Hadamard codeword. With signOf_hadamard this makes the correspondence between assignments and parity functions a bijection, so BLR's coordinate set can be handed back as an assignment.

theorem Complexity.exists_assignment_of_blr {n : ℕ} (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) (ε : ℝ) (h : BooleanAnalysis.blrAcceptProb f ≥ 1 - ε) : ∃ (a : BooleanAnalysis.Cube n), BooleanAnalysis.hammingDist f (signOf (hadamard a)) ≤ ε

Decoding. A proof passing the linearity test is close to the Hadamard encoding of an explicit assignment — the assignment the tester extracts.

Consistency forces the tensor

theorem Complexity.hadamard_basisVec {n : ℕ} (a : BooleanAnalysis.Cube n) (i : Fin n) : hadamard a (basisVec i) = a i

Reading a Hadamard table at a basis vector returns that coordinate.

theorem Complexity.tensor_basisVec {n : ℕ} (i j : Fin n) : tensor (basisVec i) (basisVec j) = basisVec (finProdFinEquiv (i, j))

The outer product of two basis vectors is the basis vector at the corresponding pair index.

theorem Complexity.eq_tensorAssign_of_consistent {n : ℕ} (a : BooleanAnalysis.Cube n) (b : BooleanAnalysis.Cube (n * n)) (h : ∀ (x y : BooleanAnalysis.Cube n), hadamard b (tensor x y) = hadamard a x * hadamard a y) : b = tensorAssign a

Consistency forces the tensor. A quadratic table that agrees with the product of the linear readings on every outer product is the tensor square of the assignment — testing at basis vectors pins down every entry. This is why the consistency check suffices: it leaves the prover no freedom in the quadratic table.

Checking a constraint

structure Complexity.QuadConstraint (n : ℕ) : Type

A quadratic constraint over 𝔽₂. Dinur's inner verifier tests exactly this: the constraints of a system with a constant-size alphabet are quadratic equations once the alphabet symbols are spelled out in bits.

• quad : BooleanAnalysis.Cube (n * n)

  The quadratic coefficients, indexed like the tensor table.

• lin : BooleanAnalysis.Cube n

  The linear coefficients.

• const : ZMod 2

  The constant term.

def Complexity.QuadConstraint.eval {n : ℕ} (C : QuadConstraint n) (a : BooleanAnalysis.Cube n) : ZMod 2

The constraint evaluated at an assignment.

Equations

• C.eval a = Complexity.hadamard (Complexity.tensorAssign a) C.quad + Complexity.hadamard a C.lin + C.const

def Complexity.QuadConstraint.Sat {n : ℕ} (C : QuadConstraint n) (a : BooleanAnalysis.Cube n) : Prop

The assignment satisfies the constraint.

Equations

• C.Sat a = (C.eval a = 0)

def Complexity.checkValue {n : ℕ} (F : BitFun (n * n)) (f : BitFun n) (C : QuadConstraint n) : ZMod 2

What the verifier computes from the two tables: one query into each.

Equations

• Complexity.checkValue F f C = F C.quad + f C.lin + C.const

theorem Complexity.checkValue_hadamard {n : ℕ} (a : BooleanAnalysis.Cube n) (C : QuadConstraint n) : checkValue (hadamard (tensorAssign a)) (hadamard a) C = C.eval a

On honest tables the check is the constraint — this is completeness.

theorem Complexity.sat_of_checks {n : ℕ} (a : BooleanAnalysis.Cube n) (b : BooleanAnalysis.Cube (n * n)) (C : QuadConstraint n) (hcons : ∀ (x y : BooleanAnalysis.Cube n), hadamard b (tensor x y) = hadamard a x * hadamard a y) (hcheck : checkValue (hadamard b) (hadamard a) C = 0) : C.Sat a

Tester soundness, exact form. If the two tables are Hadamard codewords, the consistency check holds everywhere, and the constraint check passes, then the decoded assignment satisfies the constraint. The prover's only freedom is the assignment itself: consistency pins the quadratic table to the tensor of the linear one, and then the check computes the constraint honestly.

theorem Complexity.isLinear_signOf_hadamard {n : ℕ} (a : BooleanAnalysis.Cube n) : BooleanAnalysis.IsLinear (signOf (hadamard a))

The Hadamard encoding of an assignment is linear, so it passes the linearity test with certainty.

theorem Complexity.checks_of_sat {n : ℕ} (a : BooleanAnalysis.Cube n) (C : QuadConstraint n) (h : C.Sat a) : BooleanAnalysis.blrAcceptProb (signOf (hadamard a)) = 1 ∧ (∀ (x y : BooleanAnalysis.Cube n), hadamard (tensorAssign a) (tensor x y) = hadamard a x * hadamard a y) ∧ checkValue (hadamard (tensorAssign a)) (hadamard a) C = 0

Tester completeness, exact form. The honest tables of a satisfying assignment pass the linearity test with certainty, satisfy the consistency check everywhere, and pass the constraint check.

Rigidity of the decoding

theorem Complexity.eq_of_hammingDist_lt_half {n : ℕ} {S T : Finset (Fin n)} (h : BooleanAnalysis.hammingDist (BooleanAnalysis.parityFun S) (BooleanAnalysis.parityFun T) < 1 / 2) : S = T

Distinct parity functions are far apart. Two different parity functions disagree on exactly half the cube, so agreeing on more than half forces them to be equal.

This is what makes the approximate tester work: the decoded tables are linear, and a check that passes on a large enough fraction of the cube therefore holds everywhere on the corrected tables — turning a probabilistic hypothesis into the exact one sat_of_checks needs.

theorem Complexity.hammingDist_comm {n : ℕ} (f g : BooleanAnalysis.BooleanFunction n) : BooleanAnalysis.hammingDist f g = BooleanAnalysis.hammingDist g f

theorem Complexity.hammingDist_triangle {n : ℕ} (f g h : BooleanAnalysis.BooleanFunction n) : BooleanAnalysis.hammingDist f h ≤ BooleanAnalysis.hammingDist f g + BooleanAnalysis.hammingDist g h

theorem Complexity.hadamard_inj_of_close {n : ℕ} {S T : Finset (Fin n)} {f : BooleanAnalysis.BooleanFunction n} {ε : ℝ} (hε : ε < 1 / 4) (hS : BooleanAnalysis.hammingDist f (BooleanAnalysis.parityFun S) ≤ ε) (hT : BooleanAnalysis.hammingDist f (BooleanAnalysis.parityFun T) ≤ ε) : S = T

The decoded assignment is unique: a proof cannot be close to the Hadamard encodings of two different assignments.

A nonzero linear form is balanced

theorem Complexity.chi_eq_one_sub_two (v : ZMod 2) : BooleanAnalysis.chi v = 1 - 2 * if v ≠ 0 then 1 else 0

The ±1 encoding turns a bit into 1 - 2·bit.

theorem Complexity.card_cube (n : ℕ) : Fintype.card (BooleanAnalysis.Cube n) = 2 ^ n

theorem Complexity.expect_signOf {n : ℕ} (F : BitFun n) : BooleanAnalysis.expect (signOf F) = 1 - 2 * BooleanAnalysis.prob fun (x : BooleanAnalysis.Cube n) => F x ≠ 0

The expectation of a bit function's sign encoding.

theorem Complexity.prob_hadamard_ne_zero {n : ℕ} (a : BooleanAnalysis.Cube n) (ha : a ≠ 0) : (BooleanAnalysis.prob fun (x : BooleanAnalysis.Cube n) => hadamard a x ≠ 0) = 1 / 2

A nonzero linear form is balanced. Over 𝔽₂ a nonzero linear form takes each value on exactly half the cube — the counting fact behind every "the check cannot pass too often unless it always passes" step.

The bilinear form

def Complexity.tensorRow {n : ℕ} (c : BooleanAnalysis.Cube (n * n)) (y : BooleanAnalysis.Cube n) : BooleanAnalysis.Cube n

The bilinear form of c, contracted against y: the linear form in x obtained by fixing the second argument.

Equations

• Complexity.tensorRow c y i = ∑ j : Fin n, c (finProdFinEquiv (i, j)) * y j

theorem Complexity.hadamard_tensor_row {n : ℕ} (c : BooleanAnalysis.Cube (n * n)) (x y : BooleanAnalysis.Cube n) : hadamard c (tensor x y) = hadamard (tensorRow c y) x

Row decomposition. Reading the quadratic table at an outer product is a linear reading in the first argument, with coefficients contracted against the second. This is what lets the one-variable balance lemma be applied inside a two-variable check.

theorem Complexity.prob_mono {n : ℕ} {P Q : BooleanAnalysis.Cube n → Prop} (h : ∀ (x : BooleanAnalysis.Cube n), P x → Q x) : BooleanAnalysis.prob P ≤ BooleanAnalysis.prob Q

Probability is monotone. The Fourier layer has the union bound and complements but not this.

theorem Complexity.prob_tensorRow_ne_zero {n : ℕ} (c : BooleanAnalysis.Cube (n * n)) (hc : c ≠ 0) : 1 / 2 ≤ BooleanAnalysis.prob fun (y : BooleanAnalysis.Cube n) => tensorRow c y ≠ 0

The bilinear form is nonzero on many rows. If the quadratic table's error c is nonzero, then for at least half the y the contracted linear form is nonzero — the first half of the 1/4 bound.

theorem Complexity.expect_mono {n : ℕ} {f g : BooleanAnalysis.BooleanFunction n} (h : ∀ (x : BooleanAnalysis.Cube n), f x ≤ g x) : BooleanAnalysis.expect f ≤ BooleanAnalysis.expect g

theorem Complexity.expect_const_mul {n : ℕ} (c : ℝ) (f : BooleanAnalysis.BooleanFunction n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.Cube n) => c * f x) = c * BooleanAnalysis.expect f

theorem Complexity.prob₂_tensor_ne_zero {n : ℕ} (c : BooleanAnalysis.Cube (n * n)) (hc : c ≠ 0) : 1 / 4 ≤ BooleanAnalysis.prob₂ fun (y x : BooleanAnalysis.Cube n) => hadamard c (tensor x y) ≠ 0

A nonzero bilinear form is nonzero on a quarter of all pairs. For at least half the second arguments the contracted form is nonzero, and each such form is nonzero on exactly half the first arguments.

This is the quantitative heart of the consistency check: a prover whose quadratic table differs from the tensor square fails the check on at least a quarter of the pairs, so passing it more often than that forces the tables to agree exactly.

Approximate consistency

theorem Complexity.hadamard_add {m : ℕ} (b c z : BooleanAnalysis.Cube m) : hadamard (b + c) z = hadamard b z + hadamard c z

theorem Complexity.expect_add {n : ℕ} (f g : BooleanAnalysis.BooleanFunction n) : (BooleanAnalysis.expect fun (x : BooleanAnalysis.Cube n) => f x + g x) = BooleanAnalysis.expect f + BooleanAnalysis.expect g

theorem Complexity.expect_one {n : ℕ} : (BooleanAnalysis.expect fun (x : BooleanAnalysis.Cube n) => 1) = 1

theorem Complexity.prob₂_compl {n : ℕ} (P : BooleanAnalysis.Cube n → BooleanAnalysis.Cube n → Prop) : (BooleanAnalysis.prob₂ P + BooleanAnalysis.prob₂ fun (x y : BooleanAnalysis.Cube n) => ¬P x y) = 1

theorem Complexity.eq_tensorAssign_of_prob_consistent {n : ℕ} (a : BooleanAnalysis.Cube n) (b : BooleanAnalysis.Cube (n * n)) (h : 3 / 4 < BooleanAnalysis.prob₂ fun (y x : BooleanAnalysis.Cube n) => hadamard b (tensor x y) = hadamard a x * hadamard a y) : b = tensorAssign a

Approximate consistency forces the tensor. A quadratic table passing the consistency check on more than three quarters of the pairs must be the tensor square: otherwise their difference is a nonzero bilinear form, which prob₂_tensor_ne_zero says fails on at least a quarter.

Reads over bundled randomness

theorem Complexity.prob_corrected_read_left {n : ℕ} (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) (S : Finset (Fin n)) {ε : ℝ} (hclose : BooleanAnalysis.IsClose f (BooleanAnalysis.parityFun S) ε) (x : BooleanAnalysis.Cube n) : 1 - 2 * ε ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (n + n)) => f (leftBlock z) * f (x + leftBlock z) = BooleanAnalysis.parityFun S x

A corrected read is right. Reading a close-to-linear table by self-correction, with the randomness taken from the first block of a bundled random string, returns the codeword's value except with probability 2ε.

theorem Complexity.prob_corrected_read_right {n : ℕ} (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) (S : Finset (Fin n)) {ε : ℝ} (hclose : BooleanAnalysis.IsClose f (BooleanAnalysis.parityFun S) ε) (x : BooleanAnalysis.Cube n) : 1 - 2 * ε ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (n + n)) => f (rightBlock z) * f (x + rightBlock z) = BooleanAnalysis.parityFun S x

The same for the second block.

theorem Complexity.prob_two_corrected_reads {n : ℕ} (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) (S : Finset (Fin n)) {ε : ℝ} (hclose : BooleanAnalysis.IsClose f (BooleanAnalysis.parityFun S) ε) (x x' : BooleanAnalysis.Cube n) : 1 - 4 * ε ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (n + n)) => f (leftBlock z) * f (x + leftBlock z) = BooleanAnalysis.parityFun S x ∧ f (rightBlock z) * f (x' + rightBlock z) = BooleanAnalysis.parityFun S x'

Two corrected reads are both right. The union bound over the two blocks: bundling the randomness is what makes this an ordinary one-variable union bound rather than a product-measure argument.

theorem Complexity.sat_of_prob_checks {n : ℕ} (a : BooleanAnalysis.Cube n) (b : BooleanAnalysis.Cube (n * n)) (C : QuadConstraint n) (hcons : 3 / 4 < BooleanAnalysis.prob₂ fun (y x : BooleanAnalysis.Cube n) => hadamard b (tensor x y) = hadamard a x * hadamard a y) (hcheck : checkValue (hadamard b) (hadamard a) C = 0) : C.Sat a

Tester soundness with a probabilistic consistency check. The verifier cannot test consistency everywhere — it tests one random pair. This says that is enough: passing on more than three quarters of the pairs pins the quadratic table down exactly, and then the constraint check computes the constraint honestly.

Together with checks_of_sat this is the assignment tester's guarantee at the level of decoded tables: the prover's only freedom is which assignment to encode, and if the checks pass, that assignment satisfies the constraint.

theorem Complexity.prob₂_of_forall {n : ℕ} {P : BooleanAnalysis.Cube n → BooleanAnalysis.Cube n → Prop} (h : ∀ (x y : BooleanAnalysis.Cube n), P x y) : BooleanAnalysis.prob₂ P = 1

theorem Complexity.prob_consistency_of_honest {n : ℕ} (a : BooleanAnalysis.Cube n) : (BooleanAnalysis.prob₂ fun (y x : BooleanAnalysis.Cube n) => hadamard (tensorAssign a) (tensor x y) = hadamard a x * hadamard a y) = 1

Completeness of the consistency check. The honest tables pass it on every pair, so the tester accepts a correct proof with certainty.

theorem Complexity.prob_all_reads {n m k : ℕ} (f : BooleanAnalysis.BooleanFunction n) (hf : BooleanAnalysis.IsBooleanValued f) (S : Finset (Fin n)) {ε : ℝ} (hclose : BooleanAnalysis.IsClose f (BooleanAnalysis.parityFun S) ε) (blk : Fin k → BooleanAnalysis.Cube m → BooleanAnalysis.Cube n) (hblk : ∀ (i : Fin k) (P : BooleanAnalysis.Cube n → Prop), (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube m) => P (blk i z)) = BooleanAnalysis.prob P) (pts : Fin k → BooleanAnalysis.Cube n) : 1 - ↑k * (2 * ε) ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube m) => ∀ (i : Fin k), f (blk i z) * f (pts i + blk i z) = BooleanAnalysis.parityFun S (pts i)

All of a tester's reads are correct. Given a close-to-linear table and any family of blocks of a bundled random string — each uniformly distributed, which is what hblk asks and what CubeBlocks supplies — every self-corrected read returns the codeword's value, except with probability 2kε.

Parameterising by the block maps keeps this independent of how many reads the tester makes and how the string is carved up.