Polynomial counter bounds for configuration-graph writers #
The STCON writer and the fair-coin table writer enumerate the same polynomial compact box.
configurationCounter_bounds gives a common bound for the loop counters, original input length,
and ternary symbol/count scratch register in terms of the length of the framed input.
Main results #
Turing.MultiTapeNTM.ConfigurationGraph.configurationCounter_bounds: the standard counter bound.Turing.MultiTapeNTM.ConfigurationGraph.clockedVertexBound_add_one_le_pow: the clocked box and its final counter value have a fixed polynomial bound.
theorem Turing.MultiTapeNTM.ConfigurationGraph.configurationCounter_bounds {k : ℕ} (D : ℕ) (w : List Bool) :
vertexBound (radix D w.length) + 1 ≤ ((MultiTapeTM.frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧ w.length ≤ ((MultiTapeTM.frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧ 2 ≤ ((MultiTapeTM.frame w).length + 1) ^ (D * Fintype.card (Register k) + 1)
The polynomial counter bound dominates the compact box plus one, the input length, and two. The statement includes exponent zero and the empty original word.
theorem Turing.MultiTapeNTM.ConfigurationGraph.clockedVertexBound_add_one_le_pow {k : ℕ} (D d n : ℕ) :
With the polynomial horizon Turing.polyClock d n, the full clocked compact box plus one is
bounded by a fixed power of 2 * (n + 1), including at the empty input and zero exponents.