The tower's rotation table

TowerFin gives the tower's rotation map as arithmetic on numbers; this module runs that arithmetic. A level is held as a table — one record for each vertex and dart, holding the vertex reached and the label to come back by, both in unary — and one level is computed from the one below by writing a new table whose every record needs two lookups in the old one.

The base graph's own rotation map is a table on a bounded key, so it is polynomial time however it was chosen (FiniteKey).

Main definitions

• Complexity.FinBase.tableList, Complexity.FinBase.table — a level's table
• Complexity.FinBase.baseRec — the base's rotation map, as a record
• Complexity.FinBase.stepRec — one record of the next level

Main results

• Complexity.FinBase.baseRec_mem_FP, Complexity.FinBase.stepRec_mem_FP
• Complexity.FinBase.stepRec_eq — the rule computes the level above
• Complexity.FinBase.tableStep_eq, Complexity.FinBase.tableStep_mem_FP — and writing out every record climbs one level
• Complexity.FinBase.table_mem_FP — so the table of any level is polynomial time, given room for it

theorem Complexity.mul_add_div_of_lt {a b c : ℕ} (hc : 0 < c) (h : b < c) : (a * c + b) / c = a

theorem Complexity.mul_add_mod_of_lt {a b c : ℕ} (h : b < c) : (a * c + b) % c = b

The table

noncomputable def Complexity.FinBase.tableList (F : FinBase) (k : ℕ) : List (List Bool × List Bool)

The records of the level-k table: for each vertex and dart, the vertex reached and the label pointing back, both in unary.

Equations

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

@[simp]

theorem Complexity.FinBase.length_tableList (F : FinBase) (k : ℕ) : (F.tableList k).length = F.size k * F.deg ^ 2

noncomputable def Complexity.FinBase.table (F : FinBase) (k : ℕ) : List Bool

The level-k table.

Equations

• F.table k = Complexity.DataEncode.bitstringEncode (F.tableList k)

theorem Complexity.FinBase.tableFst_table (F : FinBase) {k j : ℕ} (hj : j < F.size k * F.deg ^ 2) : tableFst (F.table k) j = List.replicate (F.rotVal k (j / F.deg ^ 2, j % F.deg ^ 2)).1 true

theorem Complexity.FinBase.tableSnd_table (F : FinBase) {k j : ℕ} (hj : j < F.size k * F.deg ^ 2) : tableSnd (F.table k) j = List.replicate (F.rotVal k (j / F.deg ^ 2, j % F.deg ^ 2)).2 true

The base graph's own table

noncomputable def Complexity.FinBase.baseRaw (F : FinBase) (z : List Bool) : List Bool

The record the base's rotation map gives, before the key is bounded.

Equations

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

def Complexity.FinBase.baseKeyBound (F : FinBase) : ℕ

How long an argument to the base's table can be.

Equations

• F.baseKeyBound = 2 * F.deg ^ 4 + 2 + F.deg

noncomputable def Complexity.FinBase.baseRec (F : FinBase) (z : List Bool) : List Bool

The base's rotation map, as a record.

Equations

• F.baseRec z = if z ∈ Complexity.keySet F.baseKeyBound fun (x : List Bool) => True then F.baseRaw z else []

theorem Complexity.FinBase.baseRec_mem_FP (F : FinBase) : F.baseRec ∈ FP

theorem Complexity.FinBase.baseRec_eq (F : FinBase) {x a : ℕ} (hx : x < F.deg ^ 4) (ha : a < F.deg) : F.baseRec (pair (List.replicate x true) (List.replicate a true)) = encPair (List.replicate (F.baseVal x a).1 true) (List.replicate (F.baseVal x a).2 true)

One record of the next level

noncomputable def Complexity.FinBase.stepRec (F : FinBase) (z : List Bool) : List Bool

One record of the level above, from the table below. The argument is pair table (unary index): the index splits into a vertex and a dart, the vertex into a vertex of the level below and a base vertex, and the dart into two base darts.

Equations

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

theorem Complexity.FinBase.stepRec_mem_FP (F : FinBase) : F.stepRec ∈ FP

theorem Complexity.FinBase.stepRec_eq (F : FinBase) {k j : ℕ} (hj : j < F.size (k + 1) * F.deg ^ 2) : F.stepRec (pair (F.table k) (List.replicate j true)) = encPair (List.replicate (F.rotVal (k + 1) (j / F.deg ^ 2, j % F.deg ^ 2)).1 true) (List.replicate (F.rotVal (k + 1) (j / F.deg ^ 2, j % F.deg ^ 2)).2 true)

The record rule computes the level above.

One level of the table

noncomputable def Complexity.FinBase.tableStep (F : FinBase) (T : List Bool) : List Bool

One level of the table: write out every record of the level above.

Equations

• F.tableStep T = Complexity.listEncFn F.stepRec (Complexity.pair (Complexity.marks (Complexity.mulC (F.deg ^ 4) (Complexity.posCount T))) T)

theorem Complexity.FinBase.tableStep_mem_FP (F : FinBase) : F.tableStep ∈ FP

theorem Complexity.FinBase.tableStep_eq (F : FinBase) (k : ℕ) : F.tableStep (F.table k) = F.table (k + 1)

theorem Complexity.FinBase.length_table_le (F : FinBase) (l : ℕ) : (F.table l).length ≤ 2 + F.size l * F.deg ^ 2 * (4 * F.size l + 4 * F.deg ^ 2 + 6)

How long a level's table is: one record a vertex and dart, and a record holds two numbers below the level's size.

Climbing to a level

theorem Complexity.FinBase.tableStep_iterate (F : FinBase) (l : ℕ) : F.tableStep^[l] (F.table 0) = F.table l

theorem Complexity.FinBase.table_mem_FP (F : FinBase) {ruler width : List Bool → List Bool} (hr : ruler ∈ FP) (hw : width ∈ FP) (hbound : ∀ (z : List Bool), ∀ l ≤ (ruler z).length, (F.table l).length ≤ (width z).length) : (fun (z : List Bool) => F.table (ruler z).length) ∈ FP

The table of a requested level is polynomial time, as soon as there is room to write it down.