The GHYS method for rigorously proving that a shadow exists is constructive. That is, one explicitly constructs a subspace around the numerical orbit which must contain a true orbit. This is essentially an interval arithmetic, or enclosure method (see, eg., [59]). In contrast, shadowing lemmas are capable of proving the existence of a shadow non-constructively [14, 15, 16, 17, 18, 60, 80]. However, they always involve computing the Jacobian of the map, or solving the variational equations of the ODE, and then estimating hyperbolicity, so they are all roughly equal in computational expense.