Guessing the certificate onto the region

The certificate is one bit per address of the region, not per register of the file: the evaluation reads its dictionary at the address whose argument blocks encode a tuple of points, and there are 2 ^ (k · nᵈ) of those, where the file has one register per block and tuple and is polynomial. So the guessing sweep is not the file-laying sweep with a different write; it is a walk over the region.

That has one consequence for its rules, and it is what this file is: the walk cannot be pointer-driven. A pointer holds a block and a tuple and can count the file's registers; it cannot count the region. So the guess is a sweep in the space-bounded program's style – one phase for the whole walk, a nondeterministic write, a step right – and its exit is a rule available at every address, so that where the guess stops is one more nondeterministic choice. Nothing has to recognize the region's end: the run a yes-instance exhibits stops at the logical top, and a run that stops earlier has left its remaining bits clear, which is a certificate like any other.

The rules are the program's own at DescriptiveComplexity.Draw.Data.regionSpec – a guess specification whose pointer never moves, so that the site's roll-over arm is the walk's every step – together with the stopping rule hasLeft_guessStop. The sweep is reachesIn_guessRegion, at the stretch's own length, and the whole phase – sweep, stop, walk home – is reachesIn_guessRegionPhase.