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').

theorem DescriptiveComplexity.Draw.card_argTag {R P K : Type} : Nat.card { τ : Tag R P K // ∃ (i : K), τ = Tag.arg i } = Nat.card K

The argument blocks are as many as the fixed-point's own indices: the k of the clock's arithmetic.

theorem DescriptiveComplexity.Draw.card_drawTag {R P K : Type} [Finite R] [Finite P] [Finite K] : Nat.card (Tag R P K) = Nat.card R + 1 + Nat.card P + Nat.card K

The tags are the program's rules, its alphabet, its phases and its blocks, so the universe is (|R| + 1 + |P| + k) · m points. The clock's own arithmetic reads that as k working blocks and |R| + 1 + |P| surplus ones – the surplus a clocked program has for free, since its rule names and its phases are tags whether it writes in them or not.

theorem DescriptiveComplexity.Draw.wideRank_lt_two_pow_logical {A R P K : Type} {dd : ℕ} [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [Finite A] [Finite R] [Finite P] [Finite K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hord : ∀ (x y : Univ A R P K dd), WMLe x y ↔ tagTupleLe x y) {s : Univ A R P K dd → Prop} (hjunk : ∀ (τ : Tag R P K), (∀ (i : K), τ ≠ Tag.arg i) → ∀ (v : Fin dd → A), ¬s (τ, v)) : wideRank s < 2 ^ (Nat.card K * Nat.card (Fin dd → A))

A logical address lies in a region of 2 ^ (k · m) addresses: its rank is below that number, k being the argument blocks and m the tuples. This is the bound every phase of a clocked program run inside the region is charged against; the counting behind it is DescriptiveComplexity.wideRank_lt_two_pow_avoids.