The Lautemann shifted-cover disjunction runs in polynomial time

Let $V(x,r)$ be a predicate decided in polynomial time by a deterministic two-tape machine of the mission's model. Consider the three-tape predicate that, on input $x$, an existential string $e$, and a universal string $u$ of length $m = |u|$, reads $e$ as a tuple of $m+1$ translation vectors $t_0,\dots,t_m \in \{0,1\}^m$ (the $i$-th vector being the length-$m$ window of $e$ starting at position $i\cdot m$, zero-padded), and asks whether

This theorem asserts that this bounded disjunction is again decidable in polynomial time. It is the second of the two machine-model closure facts needed by the Sipser–Gács–Lautemann development: it is the predicate that the $\Sigma_2^P$ characterization quantifies over, so the shifted-cover argument only produces a genuine $\Sigma_2^P$ language once this computational claim is discharged. The number of disjuncts is $m+1$ and each translation is an $m$-bit window of $e$, so the whole predicate costs $O(m)$ calls to the given machine on inputs of length at most $|x| + m$.