A ruler of logarithmic length

Amplification runs logarithmically many rounds, and the bounded-iteration rule counts rounds by the length of a string. So an algorithm needs to write a string whose length is the logarithm of its input's — the one shrinking step the rest of the development never needed.

The construction folds over the input carrying two counters: a ruler, and a threshold that doubles. Every time the number of bits read reaches the threshold, the ruler gains a mark and the threshold doubles, so the ruler counts the doublings.

Main definitions

• Complexity.logStep — one step of that fold
• Complexity.logRuler — the ruler itself

Main results

• Complexity.logRuler_mem_FP — it is an FP function

def Complexity.rulerLen : ℕ → ℕ

How long the ruler is after reading n bits: it gains a mark exactly when the count reaches the next power of two.

Equations

• Complexity.rulerLen 0 = 0
• Complexity.rulerLen n.succ = if n + 1 < 2 ^ Complexity.rulerLen n then Complexity.rulerLen n else Complexity.rulerLen n + 1

noncomputable def Complexity.logStep (z : List Bool) : List Bool

One step of the ruler fold, on pair (pair W acc) t where acc is pair ruler threshold: on reaching the threshold, add a mark and double.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.logStep_mem_FP : logStep ∈ FP

theorem Complexity.rulerLen_le (n : ℕ) : rulerLen n ≤ n

theorem Complexity.two_pow_rulerLen_le (n : ℕ) : 2 ^ rulerLen n ≤ 2 * n + 1

theorem Complexity.lt_two_pow_rulerLen (n : ℕ) : n < 2 ^ rulerLen n

theorem Complexity.log_lt_rulerLen (n : ℕ) (hn : n ≠ 0) : Nat.log 2 n < rulerLen n

The ruler is at least the binary logarithm.

theorem Complexity.rulerLen_pos {n : ℕ} (hn : 0 < n) : 0 < rulerLen n

theorem Complexity.rulerLen_le_log (n : ℕ) : rulerLen n ≤ Nat.log 2 (2 * n + 1)

The ruler is at most a logarithm: 2 ^ rulerLen n ≤ 2n + 1.

theorem Complexity.rulerLen_bigO_log {N : ℕ → ℕ} {A B : ℕ} (hN : ∀ (n : ℕ), N n ≤ A * (n + 1) ^ B) : BigO (fun (n : ℕ) => rulerLen (N n)) fun (n : ℕ) => Nat.log 2 n

A ruler over a polynomially bounded quantity is logarithmic.

theorem Complexity.logFold_eq (bound : ℕ) (z : List Bool) : 4 * z.length + 4 ≤ bound → Cobham.recFoldClamp logStep logStep bound (pair [] [true]) [] z = pair (List.replicate (rulerLen z.length) true) (List.replicate (2 ^ rulerLen z.length) true)

The fold's value after reading a list.

noncomputable def Complexity.logRulerRaw (w : List Bool) : List Bool

The fold itself, on pair W z.

Equations

• Complexity.logRulerRaw w = Complexity.Cobham.recFoldClamp Complexity.logStep Complexity.logStep (4 * w.length + 4) (Complexity.pair [] [true]) (Complexity.pairFst w) (Complexity.pairSnd w)

theorem Complexity.logRulerRaw_mem_FP : logRulerRaw ∈ FP

noncomputable def Complexity.logRuler (z : List Bool) : List Bool

A ruler of logarithmic length.

Equations

• Complexity.logRuler z = Complexity.pairFst (Complexity.logRulerRaw (Complexity.pair [] z))

theorem Complexity.logRuler_mem_FP : logRuler ∈ FP

theorem Complexity.logRuler_eq (z : List Bool) : logRuler z = List.replicate (rulerLen z.length) true

The ruler is as long as the fold says.

@[simp]

theorem Complexity.length_logRuler (z : List Bool) : (logRuler z).length = rulerLen z.length