Verifiers reading a prefix of their random string

To show that a class defined by verifiers is closed under a polynomial-time reduction f, one runs the verifier V of the target problem on the reduced instance f a. On that instance V reads q(|f a|) random or certificate bits, while the strings given for an instance a must have a length fixed by |a|. The new verifier therefore reads strings of a polynomial length P(|a|) ≥ q(|f a|) and passes their prefix of length q(|f a|) to V (Cslib.Complexity.exists_truncated_verifier). The verifier's output type is arbitrary.

Every prefix extends to the same number of longer strings, so counting through a prefix multiplies the number of accepted strings by a power of two (Cslib.Complexity.acceptCount_eq_two_pow_mul_of_take), and a bound on the fraction of strings with a property survives (Cslib.BitString.mul_two_pow_le_mul_card_filter_take).

Main results

• Cslib.Complexity.exists_truncated_verifier: a polynomial-time verifier that runs V on the reduced instance and a prefix of a polynomially long string.
• Cslib.Complexity.acceptCount_eq_two_pow_mul_of_take: accepted strings counted through a prefix.
• Cslib.BitString.mul_two_pow_le_mul_card_filter_take: a fraction bound carried through a prefix.

theorem Cslib.BitString.mul_two_pow_le_mul_card_filter_take {k K : ℕ} (hk : k ≤ K) (g : List Bool → Prop) [DecidablePred g] {c d : ℕ} (h : c * 2 ^ k ≤ d * {r : Fin k → Bool | g (List.ofFn r)}.card) : c * 2 ^ K ≤ d * {r : Fin K → Bool | g (List.take k (List.ofFn r))}.card

Fraction bounds through a prefix. If at least a c / d fraction of the strings of length k satisfy g, then at least a c / d fraction of the strings of length K ≥ k have a prefix of length k satisfying g.

theorem Cslib.Complexity.exists_truncated_verifier {α β γ : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {f : α → β} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc encB) (q : Polynomial ℕ) {V : β × List Bool → γ} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair encB Turing.MultiTapeTM.encBits) encC) : ∃ (P : Polynomial ℕ) (V' : α × List Bool → γ), Turing.MultiTapeTM.ComputableInPolyTime V' (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) encC ∧ (∀ (a : α), Polynomial.eval (encB (f a)).length q ≤ Polynomial.eval (enc a).length P) ∧ ∀ (a : α) (w : List Bool), V' (a, w) = V (f a, List.take (Polynomial.eval (encB (f a)).length q) w)

Running a verifier on a prefix. For a polynomial-time map f and a polynomial-time verifier V reading q(|f a|) bits on f a, some polynomial P bounds q(|f a|) by P(|a|), and running V on f a and the prefix of length q(|f a|) of a string is computable in polynomial time.

theorem Cslib.Complexity.acceptCount_eq_two_pow_mul_of_take {α β : Type} {V : β × List Bool → Bool} {V' : α × List Bool → Bool} {a : α} {b : β} {k K : ℕ} (hk : k ≤ K) (hV : ∀ (w : List Bool), V' (a, w) = V (b, List.take k w)) : acceptCount V' a K = 2 ^ (K - k) * acceptCount V b k

Counting through a prefix. If V' runs V on the first k bits, it accepts 2 ^ (K - k) times as many strings of length K ≥ k as V accepts strings of length k.