Finding the tower level

The expander family answers a request for n vertices with the first tower member of at least 2 n of them. An algorithm finds that member by counting: it walks up the tower, multiplying the size by deg ^ 4 at each level, and stops at the first level large enough.

The walk is one step of a loop, so Cobham.iterate_mem_FP runs it; the state is the level so far and the size so far, carried beside the requested count.

Main definitions

• Complexity.levelStep — one tick of the search

Main results

• Complexity.levelStep_iterate — what the loop has found after j ticks
• Complexity.levelStep_mem_FP — the tick is polynomial time
• Complexity.levelAfter_of_lt, Complexity.levelAfter_stable — the loop climbs until it is large enough, and then stays
• Complexity.levelAfter_snd_le — and never overshoots by more than a factor
• Complexity.levelFn_mem_FP — the search is polynomial time
• Complexity.levelFn_length — and finds the first level that is large enough
• Complexity.pow_levelFn_le — whatever level it reports, that level's size is polynomially bounded

def Complexity.levelAfter (d n : ℕ) : ℕ → ℕ × ℕ → ℕ × ℕ

The loop's own model: after j ticks, the level and the size reached.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.levelAfter d n 0 x✝ = x✝

noncomputable def Complexity.levelStep (d : ℕ) (st : List Bool) : List Bool

One tick: if the size so far is below twice the request, take another level. The state is pair (pair (level so far) (size so far)) (the request).

Equations

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

theorem Complexity.levelStep_mem_FP (d : ℕ) : levelStep d ∈ FP

theorem Complexity.levelStep_apply (d k s : ℕ) (Z : List Bool) : levelStep d (pair (pair (List.replicate k true) (List.replicate s true)) Z) = if s < 2 * Z.length then pair (pair (List.replicate (k + 1) true) (List.replicate (s * d) true)) Z else pair (pair (List.replicate k true) (List.replicate s true)) Z

theorem Complexity.levelStep_iterate (d : ℕ) (Z : List Bool) (j k s : ℕ) : (levelStep d)^[j] (pair (pair (List.replicate k true) (List.replicate s true)) Z) = pair (pair (List.replicate (levelAfter d Z.length j (k, s)).1 true) (List.replicate (levelAfter d Z.length j (k, s)).2 true)) Z

The loop's model runs the loop.

What the loop settles on

theorem Complexity.levelAfter_of_lt (d n j : ℕ) : (∀ i < j, ¬2 * n ≤ d ^ (i + 1)) → levelAfter d n j (0, d) = (j, d ^ (j + 1))

Until it is large enough, the loop is at level j with size d ^ (j + 1).

theorem Complexity.levelAfter_stable (d n : ℕ) (p : ℕ × ℕ) (j : ℕ) (h : 2 * n ≤ (levelAfter d n j p).2) (i : ℕ) : levelAfter d n (j + i) p = levelAfter d n j p

Once it is large enough, the loop stays put.

theorem Complexity.levelAfter_snd_le (d n j : ℕ) : (levelAfter d n j (0, d)).2 ≤ d + 2 * n * d

The loop never overshoots by more than a factor of d.

theorem Complexity.levelAfter_pow (d n j : ℕ) : (levelAfter d n j (0, d)).2 = d ^ ((levelAfter d n j (0, d)).1 + 1)

The size the loop carries is always the power the level names.

theorem Complexity.pow_levelAfter_le (d n j : ℕ) : d ^ ((levelAfter d n j (0, d)).1 + 1) ≤ d + 2 * n * d

The level the loop reaches names a size below d + 2 n d.

The search as one function

theorem Complexity.levelStep_iterate_shape (d : ℕ) (z : List Bool) (j : ℕ) : ∃ (K : List Bool) (S : List Bool), (levelStep d)^[j] (pair (pair [] (List.replicate d true)) z) = pair (pair K S) z ∧ K.length ≤ j ∧ S.length ≤ d + 2 * z.length * d

The shape of the state after j ticks: a level of at most j marks and a size the clamp keeps below d + 2 |z| d, beside the request.

theorem Complexity.levelStep_iterate_length_le (d : ℕ) (z : List Bool) (j : ℕ) : ((levelStep d)^[j] (pair (pair [] (List.replicate d true)) z)).length ≤ 2 * (2 * j + 2 + (d + 2 * z.length * d)) + 2 + z.length

noncomputable def Complexity.levelWidth (d : ℕ) (p : Polynomial ℕ) : Polynomial ℕ

The polynomial that bounds the loop's state.

Equations

• Complexity.levelWidth d p = Polynomial.C 4 * p + Polynomial.C (2 * d + 6) + Polynomial.C (4 * d + 1) * Polynomial.X

noncomputable def Complexity.levelFn (d : ℕ) (p : Polynomial ℕ) (z : List Bool) : List Bool

The tower level for a requested count, as one function: run the search for polynomially many ticks and read off the level.

Equations

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

theorem Complexity.levelFn_mem_FP (d : ℕ) (p : Polynomial ℕ) : levelFn d p ∈ FP

noncomputable def Complexity.sizeFn (d : ℕ) (p : Polynomial ℕ) (z : List Bool) : List Bool

The size at the level the search reports.

Equations

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

theorem Complexity.sizeFn_mem_FP (d : ℕ) (p : Polynomial ℕ) : sizeFn d p ∈ FP

theorem Complexity.sizeFn_length (d : ℕ) (p : Polynomial ℕ) (z : List Bool) : (sizeFn d p z).length = d ^ ((levelFn d p z).length + 1)

The size the search reports is the power its level names.

theorem Complexity.levelFn_length (d : ℕ) (p : Polynomial ℕ) (z : List Bool) (L : ℕ) (hL : 2 * z.length ≤ d ^ (L + 1)) (hmin : ∀ i < L, ¬2 * z.length ≤ d ^ (i + 1)) (hp : L ≤ Polynomial.eval z.length p) : (levelFn d p z).length = L

The search finds the first level that is large enough.

theorem Complexity.pow_levelFn_le (d : ℕ) (p : Polynomial ℕ) (z : List Bool) : d ^ ((levelFn d p z).length + 1) ≤ d + 2 * z.length * d

Whatever level the search reports, its size is bounded — which is what lets the table at that level be written down.