The file a clocked program lays out

A space-bounded program gives every element of its universe a register (DescriptiveComplexity.segFile), and laying that file out costs one sweep of it. A program on a clock cannot pay that: a rule sees the control and the cell under the head and nothing else, so the only stretches it can walk are a fixed number of tuple roll-overs long, and the universe is |Tag| of those with |Tag| the program's own rule count.

What it can afford is one register per block and tuple, which is also all that a register's contents ever depend on: the block one-hot goes through DescriptiveComplexity.Draw.tagBlk alone and the name slots are the tuple, so nothing of a tag beyond its block is ever read back (DescriptiveComplexity.Draw.Data.ixBack). This file is that file: DescriptiveComplexity.blkFile, one register per DescriptiveComplexity.Wide.BlkIx, laid out on a stretch of consecutive addresses in the block-major order DescriptiveComplexity.Wide.blkLe.

Everything it needs is already general – the interface (DescriptiveComplexity.IxFile), the walks over it, the construction on a stretch (DescriptiveComplexity.ixSegFile) and the background (DescriptiveComplexity.Draw.Data.ixBack) – so all that is added here is the instantiation and the two numbers a caller has to check: how many registers there are, and that the stretch fits.

noncomputable def DescriptiveComplexity.blkFile (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (U : Type) [FirstOrder.Language.wide.Structure U] [Finite U] (dd : ℕ) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx K A dd) ≤ Nat.card { p : WPoint U // (wideData U).Posn p }) : IxFile U (Wide.BlkIx K A dd) (Wide.blkLe K A dd)

The file a clocked program lays out: one register per block and tuple, on the stretch of consecutive addresses whose ranks start at base.

Equations

• DescriptiveComplexity.blkFile A K U dd h hpos hbase = DescriptiveComplexity.ixSegFile (DescriptiveComplexity.Wide.blkLe K A dd) h ⋯ hpos hbase

theorem DescriptiveComplexity.card_blkFile {A K : Type} [Finite K] (dd : ℕ) : Nat.card (Wide.BlkIx K A dd) = (Nat.card K + 1) * Nat.card (Fin dd → A)

How many registers the file has: one per block, one more for the blockless ones, times the tuples. This is the number the stretch has to fit, and the number of tuple roll-overs the laying sweep runs for.

Walking the file: the pointer's advance and its two ends

The sweep that lays the file out carries the register it is at in the machine's control, and a rule advances it: dstSt is a function of the control, so the next register has to be a function of the current one, not merely to exist. These three are that function and the two ends its walk runs between; nothing here is computed – a rule's fields are semantic – so the choice off DescriptiveComplexity.exists_ixSucc is the definition, and its characterization is what a caller discharges the walk with.

noncomputable def DescriptiveComplexity.blkNext (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) (u : Wide.BlkIx K A dd) : Wide.BlkIx K A dd

The next register: the successor of an index in the layout order, and the index itself at the top of it.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.ixSucc_blkNext (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) {u : Wide.BlkIx K A dd} (hne : ∃ (v : Wide.BlkIx K A dd), WMLt (Wide.blkLe K A dd) u v) : IxSucc (Wide.blkLe K A dd) u (blkNext A K dd u)

The advance is the layout order's successor, wherever there is one.

theorem DescriptiveComplexity.blkNext_of_top (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) {u : Wide.BlkIx K A dd} (htop : ∀ (v : Wide.BlkIx K A dd), Wide.blkLe K A dd v u) : blkNext A K dd u = u

The advance stops at the top, which is what makes the sweep's last round recognizable without a second test.

noncomputable def DescriptiveComplexity.blkBot (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] : Wide.BlkIx K A dd

The first register: least in the layout order, where the laying sweep's pointer starts.

Equations

• DescriptiveComplexity.blkBot A K dd = ⋯.choose

noncomputable def DescriptiveComplexity.blkTop (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] : Wide.BlkIx K A dd

The last register: greatest in the layout order, where it stops.

Equations

• DescriptiveComplexity.blkTop A K dd = ⋯.choose

theorem DescriptiveComplexity.blkLe_blkBot (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] (v : Wide.BlkIx K A dd) : Wide.blkLe K A dd (blkBot A K dd) v

The first register is below every register.

theorem DescriptiveComplexity.blkLe_blkTop (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] (v : Wide.BlkIx K A dd) : Wide.blkLe K A dd v (blkTop A K dd)

Every register is below the last.

theorem DescriptiveComplexity.ixSucc_blkNext_of_ne (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] {u : Wide.BlkIx K A dd} (hu : u ≠ blkTop A K dd) : IxSucc (Wide.blkLe K A dd) u (blkNext A K dd u)

The advance stops exactly at the last register, so the walk's stop test is the pointer reaching DescriptiveComplexity.blkTop.

noncomputable def DescriptiveComplexity.tupTop (A : Type) [LinearOrder A] [Finite A] (dd : ℕ) [Nonempty A] : Fin dd → A

The last tuple: greatest in the tuples' own lexicographic order. A pointer holding it is at the last register of its block, which is what a roll-over's guard reads.

Equations

• DescriptiveComplexity.tupTop A dd = ⋯.choose

theorem DescriptiveComplexity.tupLeLex_tupTop (A : Type) [LinearOrder A] [Finite A] (dd : ℕ) [Nonempty A] (v : Fin dd → A) : tupLeLex v (tupTop A dd)

Every tuple is below the last.

noncomputable def DescriptiveComplexity.blkNextB (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] (b : Option K) : Option K

The next block: the block of the register after the last of this one. A destination phase is a constant, so a roll-over rule needs the next block as a function of the current one alone, and this is it.

Equations

• DescriptiveComplexity.blkNextB A K dd b = (DescriptiveComplexity.blkNext A K dd (b, DescriptiveComplexity.tupTop A dd)).1

theorem DescriptiveComplexity.blkNext_fst_of_ne_tupTop (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] {u : Wide.BlkIx K A dd} (hu : u.2 ≠ tupTop A dd) : (blkNext A K dd u).1 = u.1

Within a block the advance stays in it: below the last tuple the next register is the same block's, so the stepping rule keeps its phase and only the roll-over changes it.

theorem DescriptiveComplexity.snd_blkTop (A K : Type) [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] (dd : ℕ) [Nonempty A] : (blkTop A K dd).2 = tupTop A dd

The last register's tuple is the last tuple: the order is block-major, so the greatest index is the greatest tuple of the greatest block. This is what makes the sweep's stop test – the pointer holds the last tuple and the last register – fire at one place.

The stretch fits

The one arithmetic fact a caller of DescriptiveComplexity.blkFile owes: the file has fewer registers than the universe has elements – a block and a tuple is an element of the universe, the blockless register taking the alphabet tag – and the addresses are 2 ^ that, so a stretch based at 1 always fits.

def DescriptiveComplexity.blkTag (R P K : Type) : Option K → Draw.Tag R P K

The blockless register and each block, as tags: the alphabet tag stands for the blockless one.

Equations

• DescriptiveComplexity.blkTag R P K none = DescriptiveComplexity.Draw.Tag.sym
• DescriptiveComplexity.blkTag R P K (some k) = DescriptiveComplexity.Draw.Tag.arg k

theorem DescriptiveComplexity.blkTag_injective (R P K : Type) : Function.Injective (blkTag R P K)

The address a clocked file's marks stand for

A mark on the file is an address of the tape (DescriptiveComplexity.ixAddr), and the correspondence is what lets a program hold an address it cannot see – the one under its head – on registers it can. It is only used on the argument registers, and the two conditions of DescriptiveComplexity.wmIncr_ixAddr hold of exactly those: the argument tags are the greatest ones (DescriptiveComplexity.Draw.lt_arg), so nothing the file has no register for lies above an argument element, and the block order was chosen to make DescriptiveComplexity.blkTag monotone.

def DescriptiveComplexity.blkIxElt {A : Type} (R P : Type) {K : Type} (dd : ℕ) (u : Wide.BlkIx K A dd) : Draw.Univ A R P K dd

The element a register holds the bit of.

Equations

• DescriptiveComplexity.blkIxElt R P dd u = (DescriptiveComplexity.blkTag R P K u.1, u.2)

def DescriptiveComplexity.BlkIxUse (A K : Type) (dd : ℕ) (u : Wide.BlkIx K A dd) : Prop

The registers an address uses: the argument blocks, the blockless ones standing for the alphabet tag and never entering a logical address.

Equations

• DescriptiveComplexity.BlkIxUse A K dd u = ∃ (k : K), u.1 = some k

theorem DescriptiveComplexity.blkTag_lt_iff {R P K : Type} [LinearOrder R] [LinearOrder P] [LinearOrder K] {b b' : Option K} : Wide.blkTagLe K b b' ∧ b ≠ b' ↔ blkTag R P K b < blkTag R P K b'

A block is below another exactly when its tag is: the block order was built for this, the blockless registers taking the alphabet tag, which the argument tags all sit above.

theorem DescriptiveComplexity.blkLe_iff_tagTupleLe {A R P K : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] (dd : ℕ) (u u' : Wide.BlkIx K A dd) : Wide.blkLe K A dd u u' ↔ tagTupleLe (blkIxElt R P dd u) (blkIxElt R P dd u')

The register order is the element order: the block order was built for it.

theorem DescriptiveComplexity.blkIxElt_mono {A R P K : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] (dd : ℕ) [FirstOrder.Language.wide.Structure (Draw.Univ A R P K dd)] (hord : ∀ (x y : Draw.Univ A R P K dd), WMLe x y ↔ tagTupleLe x y) (u u' : Wide.BlkIx K A dd) : WMLt (Wide.blkLe K A dd) u u' ↔ WMLt WMLe (blkIxElt R P dd u) (blkIxElt R P dd u')

The register order is the element order, strictly.

theorem DescriptiveComplexity.blkIxElt_up {A R P K : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] (dd : ℕ) [FirstOrder.Language.wide.Structure (Draw.Univ A R P K dd)] (hord : ∀ (x y : Draw.Univ A R P K dd), WMLe x y ↔ tagTupleLe x y) {u : Wide.BlkIx K A dd} (hu : BlkIxUse A K dd u) {x : Draw.Univ A R P K dd} (hlt : WMLt WMLe (blkIxElt R P dd u) x) : ∃ (u' : Wide.BlkIx K A dd), BlkIxUse A K dd u' ∧ blkIxElt R P dd u' = x

Nothing without a register lies above an argument element: the argument tags come last, so the elements the file names are upward closed and the addresses over them are an initial interval of the tape.