Counting out 2 ^ r n in unary

A verifier using r n coins has 2 ^ r n coin strings, and an algorithm that has to look at all of them needs that many steps counted out somewhere. When r is logarithmic the count is polynomial, so a polynomial-time function can write it down — by starting from a single mark and doubling r n times.

The hypothesis is the one Constructible supplies: r n itself is available in unary in polynomial time.

Main definitions

• Complexity.dbl — doubling a string

Main results

• Complexity.exists_poly_two_pow_of_bigO_log — 2 ^ O(log n) is polynomial
• Complexity.unaryExp_mem_FP — 2 ^ r n marks, in polynomial time

def Complexity.dbl (s : List Bool) : List Bool

Doubling: the string followed by itself.

Equations

• Complexity.dbl s = s ++ s

theorem Complexity.dbl_mem_FP : dbl ∈ FP

theorem Complexity.dbl_iterate (n : ℕ) : dbl^[n] [true] = List.replicate (2 ^ n) true

theorem Complexity.exists_poly_two_pow_of_bigO_log {r : ℕ → ℕ} (h : BigO r fun (n : ℕ) => Nat.log 2 n) : ∃ (p : Polynomial ℕ), ∀ (n : ℕ), 2 ^ r n ≤ Polynomial.eval n p

A logarithmic exponent gives a polynomial. This is what makes a O(log n) randomness bound usable: the number of coin strings stays polynomial.

theorem Complexity.unaryExp_mem_FP {r : ℕ → ℕ} (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) (p : Polynomial ℕ) (hp : ∀ (n : ℕ), 2 ^ r n ≤ Polynomial.eval n p) : (fun (x : List Bool) => List.replicate (2 ^ r x.length) true) ∈ FP

Writing 2 ^ r n marks. If the number of coins is available in unary in polynomial time and the number of coin strings is polynomially bounded, then that many marks can be written in polynomial time.

theorem Complexity.unaryExp_mem_FP_of_bigO_log {r : ℕ → ℕ} (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) (h : BigO r fun (n : ℕ) => Nat.log 2 n) : (fun (x : List Bool) => List.replicate (2 ^ r x.length) true) ∈ FP

The form the assembly uses. A constructible logarithmic randomness bound lets the number of coin strings be counted out in polynomial time.