The answer vector of a short answer determines it #
answerVec F m a reads the tape holding a followed by blanks at the 2^m positions the m-bit
strings number. When the tape's a fits in the first half of those positions, 2 |a| ≤ 2^m, the
vector determines a (answerVec_injective): each cell c < 2^{m-1} is read off its two
positions, and the cells beyond hold blanks for both strings. The soundness of answer reduction
decodes the answer polynomials of a PCP proof this way.
theorem
MIPRE.SAT.exists_bitsVal_ofFn
(m p : ℕ)
(hp : p < 2 ^ m)
:
∃ (w : Fin m → Bool), Cost.bitsVal (List.ofFn w) = p
Every position is numbered by an m-bit string.
theorem
MIPRE.SAT.answerVec_injective
{F : Type u_1}
[CommRing F]
[Nontrivial F]
(m : ℕ)
{a b : Cost.BitStr}
(ha : 2 * List.length a ≤ 2 ^ m)
(hb : 2 * List.length b ≤ 2 ^ m)
(h : answerVec F m a = answerVec F m b)
:
The answer vector of a short answer determines it.