Length comparison decided in linear time by multi-tape Turing machine
ProvedCookLevin.lengthCheck_machine_linearcost-modellength-checklinear-timeturing-machine
There exists a multi-tape Turing machine with tape count and alphabet size that decides whether the certificate has length at most the instance :
within a linear number of steps for some constant .
The machine operates by simultaneously advancing the heads on tape 0 (holding ) and tape 1 (holding ) one cell per step until encountering a blank symbol. If the certificate head reaches a blank while the instance head is still reading input bits (or simultaneously reaches a blank), holds and the machine writes (true) to cell 1 of the verdict tape. If the instance head encounters a blank first, and the machine writes (false). The total step count is bounded by .
Preamble
import Definitions.Def_CookLevin_Cost
Formal statement
namespace CookLevin
theorem lengthCheck_machine_linear :
∃ (M : Machine) (k G : Nat) (c0 : Nat),
TuringMachine k G M ∧
∀ x w : List Bool,
DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
(c0 * (x.length + w.length + 1))
(decide (w.length ≤ x.length)) := by sorry
end CookLevinSource