The region a clocked program works in, and its size

The universe a Draw.Data reduction draws is Draw.Tag R P K × (Fin dd → A), and a logical address – one whose non-argument blocks are empty (DescriptiveComplexity.Draw.logicalTop) – is exactly an address of the working region: the non-argument tags are the most significant, so the logical addresses are an initial stretch of the tape (DescriptiveComplexity.wmAvoids_of_wmSetLe).

What a clocked program needs of that region is its size, since every phase it runs inside it is charged against it and a bound by the number of addresses is a bound by the clock itself. wideRank_lt_two_pow_logical is that size: a logical address has rank below 2 ^ (k · m), with k the number of argument blocks and m the number of tuples – the two numbers the clock's own arithmetic is written in (DescriptiveComplexity.Draw.Data.nexTotal_lt_two_pow').