The expander's table, for a requested size

AlgLevel finds the tower level a request calls for, and TowerTable writes the rotation table of a level. Putting the two together writes the table of the level a request calls for — and it is polynomially long, because the level the search reports always names a size within a constant factor of the request.

Main definitions

• Complexity.FinBase.famTableFn — the table for a requested size

Main results

• Complexity.FinBase.famTableFn_mem_FP — writing it is polynomial time
• Complexity.FinBase.famRotFn_mem_FP — and the family's rotation map is polynomial time
• Complexity.FinBase.levelFn_fitLevel — the search reports the level the family uses

noncomputable def Complexity.FinBase.searchLevel (F : FinBase) (p : Polynomial ℕ) (z : List Bool) : ℕ

The level the search reports for a request.

Equations

• F.searchLevel p z = (Complexity.levelFn (F.deg ^ 4) p z).length

theorem Complexity.FinBase.size_searchLevel_le (F : FinBase) (p : Polynomial ℕ) (z : List Bool) : F.size (F.searchLevel p z) ≤ F.deg ^ 4 + 2 * z.length * F.deg ^ 4

The size at the reported level is within a constant factor of the request.

theorem Complexity.FinBase.size_le_of_le (F : FinBase) (p : Polynomial ℕ) {l : ℕ} (z : List Bool) (hl : l ≤ F.searchLevel p z) : F.size l ≤ F.deg ^ 4 + 2 * z.length * F.deg ^ 4

noncomputable def Complexity.FinBase.famTableFn (F : FinBase) (p : Polynomial ℕ) (z : List Bool) : List Bool

The table of the level a request calls for.

Equations

• F.famTableFn p z = F.table (F.searchLevel p z)

noncomputable def Complexity.FinBase.tableWidth (F : FinBase) : Polynomial ℕ

The polynomial that bounds that table.

Equations

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

theorem Complexity.FinBase.eval_tableWidth (F : FinBase) (n : ℕ) : Polynomial.eval n F.tableWidth = 2 + (F.deg ^ 4 + 2 * F.deg ^ 4 * n) * F.deg ^ 2 * (4 * (F.deg ^ 4 + 2 * F.deg ^ 4 * n) + (4 * F.deg ^ 2 + 6))

theorem Complexity.FinBase.famTableFn_mem_FP (F : FinBase) (p : Polynomial ℕ) : F.famTableFn p ∈ FP

Writing the table for a requested size is polynomial time.

The level the family asks for

theorem Complexity.FinBase.levelFn_fitLevel (F : FinBase) (p : Polynomial ℕ) (hd : 1 < F.deg) (n : ℕ) (hp : F.fitLevel hd n ≤ Polynomial.eval n p) : (levelFn (F.deg ^ 4) p (List.replicate n true)).length = F.fitLevel hd n

The search reports the level the family uses.

theorem Complexity.FinBase.sizeFn_fitN (F : FinBase) (p : Polynomial ℕ) (hd : 1 < F.deg) (n : ℕ) (hp : F.fitLevel hd n ≤ Polynomial.eval n p) : (sizeFn (F.deg ^ 4) p (List.replicate n true)).length = F.fitN hd n

The search reports the size the family uses.

theorem Complexity.FinBase.famTableFn_eq (F : FinBase) (p : Polynomial ℕ) (hd : 1 < F.deg) (n : ℕ) (hp : F.fitLevel hd n ≤ Polynomial.eval n p) : F.famTableFn p (List.replicate n true) = F.table (F.fitLevel hd n)

And writes that level's table.

The family's rotation map

noncomputable def Complexity.FinBase.famRotFn (F : FinBase) (p : Polynomial ℕ) (z : List Bool) : List Bool

The family's rotation map, on pair (unary n) (pair (unary v) (unary i)): split the dart into a slot and a step, lift the vertex into the tower member, look the step up in that member's table, and fold the answer back onto n vertices. Darts past the fold's degree are self-loops.

Equations

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

theorem Complexity.FinBase.famRotFn_mem_FP (F : FinBase) (p : Polynomial ℕ) : F.famRotFn p ∈ FP

theorem Complexity.FinBase.famRotFn_eq (F : FinBase) (p : Polynomial ℕ) (hd : 1 < F.deg) (n v i : ℕ) (hn : 0 < n) (hp : F.fitLevel hd n ≤ Polynomial.eval n p) : F.famRotFn p (pair (List.replicate n true) (pair (List.replicate v true) (List.replicate i true))) = pair (List.replicate (F.famRotVal hd n (v, i)).1 true) (List.replicate (F.famRotVal hd n (v, i)).2 true)

The rotation function runs the family's rotation map.