The Hadamard tester, as it actually runs #
Complexitylib.Classes.PCP.Internal.Hadamard analyses the tester at the
decoded level: its statements are about the codewords hadamard a and
hadamard b that the two proof tables are supposed to be. A tester cannot read
those. It reads the tables it is given, which are only close to codewords, and
it recovers codeword values by self-correction — reading two nearby entries and
multiplying.
This module closes that gap. The tester's whole random string is one point of a
bundled cube (CubeBlocks): the first block picks the two query points, and the
remaining blocks supply one correction string per read. Every read is then
correct except with probability 2ε, the failures are collected by a union
bound, and prob_le_of_imp_of_good transfers the observed acceptance
probability to the decoded check that Hadamard already knows how to use.
The one wrinkle is that the consistency check is bilinear over 𝔽₂, not
multiplicative on signs: ⟨a ⊗ a, x ⊗ y⟩ = ⟨a, x⟩ · ⟨a, y⟩ is a product of
bits, and chi does not carry products of bits to products of signs. So the
reads' ±1 answers are converted back to bits by signBit before being
compared, which is exactly how the check is stated in the literature.
Main definitions #
Complexity.signBit— the bit a±1answer stands forComplexity.TesterAccepts— the tester's check on the raw tablesComplexity.ReadsCorrect— the event that every self-corrected read is right
Main results #
Complexity.prob_reads_correct— every read is right except with probability4ε + 2ε'Complexity.prob_testerAccepts_of_honest— completeness: the honest proof is accepted alwaysComplexity.sat_of_prob_tester— soundness of the tester as it runs: if the raw tables are close to codewords and the raw check passes often enough, the decoded assignment satisfies the constraintComplexity.exists_sat_of_prob_tester— the same with nothing assumed about the proof: BLR supplies the closeness
Reading a sign as a bit #
The bit a ±1 answer stands for.
Instances For
Signs and bits correspond: signBit inverts chi.
A self-corrected read is right. The decoded-level restatement of
local_correctability: the value returned is the codeword's bit, read as a
sign.
The tester #
The first query point: the second half of the query block.
Equations
Instances For
The second query point: the first half of the query block.
Equations
Instances For
The correction string for the first read of the linear table.
Equations
Instances For
The correction string for the second read of the linear table.
Equations
Instances For
The correction string for the read of the quadratic table.
Equations
Instances For
The tester's check, made on the raw tables: the self-corrected value of
the quadratic table at x ⊗ y must be the product, as bits, of the
self-corrected values of the linear table at x and at y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The event that all three self-corrected reads return the codeword's value.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every read is right, at once. The query points are chosen by the first
block and the corrections by the rest, so prob_blocks_ge fixes the points
before the corrections are drawn and the three failure probabilities simply
add.
Consistency forces the tensor, on raw tables. The consistency check passing often enough on tables close to codewords forces the quadratic codeword to be the tensor square of the linear one.
Soundness of the tester as it runs. Raw tables close to Hadamard codewords, a raw check passing on more than three quarters of the randomness (with room for the reads' failure probability), and a constraint satisfied by the decoded tables together force the decoded assignment to satisfy the constraint.
The gap 4ε + 2ε' is the price of self-correction: three reads, each wrong
with probability at most twice the table's distance from its codeword.
Completeness #
A Hadamard codeword is linear in the query point.
Self-correction is exact on an honest table. The two reads are
chi ⟨a, r⟩ and chi (⟨a, x⟩ + ⟨a, r⟩), and their product telescopes because
chi turns the 𝔽₂ sum into a product of signs and 2⟨a, r⟩ = 0.
The honest proof passes every read.
Completeness of the tester as it runs. The honest proof — the Hadamard encoding of an assignment together with the encoding of its tensor square — is accepted on every random string, so with probability one.
The honest proof is accepted with probability one.
The constraint check #
The tester's constraint check, made on the raw tables: the constraint's
quadratic part is read from g, its linear part from f, both by
self-correction, and the two bits plus the constant must cancel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Both reads of the constraint check are right except with probability
2ε + 2ε'.
The constraint check is decisive. Its conclusion — that the decoded tables satisfy the constraint — does not depend on the randomness, so it is enough that some random string both passes the check and has correct reads. That happens as soon as the check passes more often than the reads fail.
Soundness with nothing assumed about the proof #
The Hadamard assignment tester is sound. Nothing is assumed about the two tables: linearity is what the BLR test establishes, and the assignment is what its soundness decodes. A proof passing all three tests often enough certifies that the constraint is satisfiable.
This is the inner verifier Dinur's alphabet-reduction step composes with: its proof length and query count do not depend on the outer system at all, only on the constant-size constraint being checked.