Finite-alphabet multitape polynomial time is canonical P #
The explicit binary simulator takes at most 2 * n + T + 3 CSLib steps for a source
computation of T steps. The existing CSLib-to-complexitylib simulation then transfers
polynomial-time membership to complexitylib's fixed-alphabet, one-sided machine model.
theorem
Complexity.DepthThreeLowerBound.FiniteMultiTapeBridge.computes
(M : FiniteMultiTapeMachine)
(w : List Bool)
(b : Bool)
(T : ℕ)
(h : MultiTapeHaltsIn M w b T)
:
(machine M).ComputesInTimeAndSpace w [b] (2 * w.length + T + 3)
(Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg w) (2 * w.length + T + 3))
The simulator emits the source verdict with a linear input-initialization overhead.
theorem
Complexity.DepthThreeLowerBound.FiniteMultiTapeMachine.mem_P
{M : FiniteMultiTapeMachine}
{L : List Bool → Bool}
{p : Polynomial ℕ}
(h : ∀ (w : List Bool), MultiTapeHaltsIn M w (L w) (Polynomial.eval w.length p))
:
A polynomial-time source decider establishes membership in complexitylib's P.