The background: the machine's mutable state, presented as a tape

Every kit discharge takes a family of slot equations – the register mark is set exactly at the register cells, the marker at one working-area address, and so on. They are all facts about one object: the machine's mutable state – its registers, its stage tracks, its markers – laid over the permanent marks of DescriptiveComplexity.Draw.slotMark. This file is that object, DescriptiveComplexity.Draw.TapeSt, its presentation DescriptiveComplexity.Draw.Data.back as the rest family the pass layer walks, and the slot equations, proved once: the discharges of DrawRun will cite them instead of re-deriving per call site.

The split of a track's home: the four machine registers (mir, tgt, sav, val) hold bits per element – their digit at a cell is DescriptiveComplexity.regBit, set only at register cells – while the stage tracks (old i, new i) and the working-area markers (wk, bot, ltp) hold bits per cell, anywhere on the tape. The permanent mark slots (reg, the ends, blk, name, pdd) read DescriptiveComplexity.Draw.slotMark at register cells and are clear elsewhere, which is what their read-back equations say.

What indexes the file is a parameter. DescriptiveComplexity.Draw.Data.ixBack reads a background at an arbitrary index, because a program on a clock cannot give every element of the universe a register and nothing here needs it to: a slot depends on the register's block, on the tuple it names, on where it sits in the layout order, and on nothing else about the index. The state carries the index with it – the four machine registers hold a bit per register and the stage tracks and markers a bit per cell, so DescriptiveComplexity.Draw.TapeSt takes the index and DescriptiveComplexity.Draw.TapeStD is the elementwise case. DescriptiveComplexity.Draw.Data.back is that at the diagonal – the index the universe itself, the order its own – which is what a space-bounded program uses, and every slot equation below is stated there. The two ends are already general (DescriptiveComplexity.Draw.Data.ixBack_regFirst, DescriptiveComplexity.Draw.Data.ixBack_regLast): which cell carries them is a fact about the layout order and about nothing else.

structure DescriptiveComplexity.Draw.TapeSt {L : FirstOrder.Language} (dt : Data L) (A R' P' I : Type) : Type 1

The machine's mutable state: the four registers (bits per element), the stage tracks and markers (bits per cell). The permanent marks are not here – they never change.

• mir : I → Prop

  The MIRROR register.

• tgt : I → Prop

  The TARGET register.

• sav : I → Prop

  The SAV register.

• val : I → Prop

  The VAL register.

• old : dt.d.B.ι → (Univ A R' P' dt.KIx dt.dd → Prop) → Prop

  The current stage of each variable, a bit per cell.

• new : dt.d.B.ι → (Univ A R' P' dt.KIx dt.dd → Prop) → Prop

  The next stage of each variable, a bit per cell.

• wk : (Univ A R' P' dt.KIx dt.dd → Prop) → Prop

  The working-cell marker, a bit per cell.

• bot : (Univ A R' P' dt.KIx dt.dd → Prop) → Prop

  The bottom marker, a bit per cell.

• ltp : (Univ A R' P' dt.KIx dt.dd → Prop) → Prop

  The end marker of the logical interval, a bit per cell.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.TapeStD {L : FirstOrder.Language} (dt : Data L) (A R' P' : Type) : Type 1

The machine's state at the elementwise file: one register per element of the universe, which is what a space-bounded program has.

Equations

• DescriptiveComplexity.Draw.TapeStD dt A R' P' = DescriptiveComplexity.Draw.TapeSt dt A R' P' (DescriptiveComplexity.Draw.Univ A R' P' dt.KIx dt.dd)

def DescriptiveComplexity.Draw.padTup {L : FirstOrder.Language} {dt : Data L} {A : Type} (zero : A) (c : Fin dt.dd0 → A) : Fin dt.dd → A

The tuple a control names: the coordinates it computes below dd₀, the designated zero above – the canonical padding of every register a scan by name stops at.

Equations

• DescriptiveComplexity.Draw.padTup zero c j = if h : ↑j < dt.dd0 then c ⟨↑j, h⟩ else zero

structure DescriptiveComplexity.Draw.Layout {L : FirstOrder.Language} (dt : Data L) (A R' P' I : Type) : Type

What a register file is, as the background reads it: the cells, the order they are laid out in, the block each register belongs to and the tuple it names. Those four are everything a slot depends on, and none of them asks the index to be the universe.

Bundled rather than passed one at a time because the whole evaluation layer carries it, and because a bare family of cells is what a definition can take: a register file carries proofs as well, and only the statements need those.

• cell : I → Univ A R' P' dt.KIx dt.dd → Prop

  The address of the register an index names.

• le : I → I → Prop

  The order the registers are laid out in.

• blk : I → Option dt.KIx

  The block a register belongs to.

• arg : I → Fin dt.dd → A

  The tuple a register names.

def DescriptiveComplexity.Draw.Layout.NameSep {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) (zero : A) (hdd : dt.dd0 ≤ dt.dd) : Prop

A layout whose registers are told apart by their marks: two registers of one and the same block, both canonically padded, whose named coordinates agree, are the same register.

This is what a navigation-by-name scan asks of its stopping condition, and it is where a layout does real work: the elementwise one has it because a register is its tag and its tuple, and a clocked program's file has it because its index carries the block and the tuple and nothing else.

Equations

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

def DescriptiveComplexity.Draw.Layout.HasName {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) (zero : A) : Prop

A layout with a register for every named tuple: whatever block and whatever tuple the control names, some register carries them.

This is the second half of what a navigation-by-name scan needs – NameSep says the name identifies at most one register, this says it identifies at least one – and it is what a clocked program's file is built to have: its index is the pair of a block and a tuple.

The tuples asked for are the named ones, DescriptiveComplexity.Draw.padTup of what a control holds: a mark carries dd₀ coordinates and nothing reads a register's tuple above them, so a file that has one register per named tuple has every register the machine can navigate to, and is smaller than one per tuple by the factor the padding accounts for.

Equations

• lay.HasName zero = ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), ∃ (u : I), lay.blk u = some b ∧ lay.arg u = DescriptiveComplexity.Draw.padTup zero c

noncomputable def DescriptiveComplexity.Draw.Layout.reg {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) {zero : A} (hhas : lay.HasName zero) (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A) : I

The register a name picks out: the one HasName provides, chosen. A layout that also has NameSep has only one, so this is the register of the block and the tuple, and everything the evaluation layer reads at «the cell of this tuple» is read here.

Chosen rather than a field, because the two properties are what a file has to prove and this adds nothing to them.

Equations

• lay.reg hhas b c = ⋯.choose

structure DescriptiveComplexity.Draw.LaidFile {L : FirstOrder.Language} (dt : Data L) (A R' P' I : Type) [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : Type

A register file together with its layout: the cells, the order they are laid out in, the block each register belongs to and the tuple it names, plus the two conditions that make a family of addresses a file – the cells grow with the index, and none of them is empty.

This is what the evaluation layer carries. The kits ask for the file alone (DescriptiveComplexity.Draw.LaidFile.toIxFile) and the background for the layout alone (DescriptiveComplexity.Draw.LaidFile.toLayout); carrying the two together is what lets one parameter stand where DescriptiveComplexity.RegFile stood.

• cell : I → Univ A R' P' dt.KIx dt.dd → Prop

  The address of the register an index names.

• le : I → I → Prop

  The order the registers are laid out in.

• blk : I → Option dt.KIx

  The block a register belongs to.

• arg : I → Fin dt.dd → A

  The tuple a register names.

• strictMono (u v : I) : WMLt self.le u v → WMSetLt WMLe (self.cell u) (self.cell v)

  Registers laid out later have strictly greater addresses.

• cell_nonempty (u : I) : ∃ (x : Univ A R' P' dt.KIx dt.dd), self.cell u x

  No register's address is empty.

@[reducible]

def DescriptiveComplexity.Draw.LaidFile.toLayout {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] (F : LaidFile dt A R' P' I) : Layout dt A R' P' I

The layout of a laid file: what the background reads.

Equations

• F.toLayout = { cell := F.cell, le := F.le, blk := F.blk, arg := F.arg }

@[reducible]

def DescriptiveComplexity.Draw.LaidFile.toIxFile {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] (F : LaidFile dt A R' P' I) : IxFile (Univ A R' P' dt.KIx dt.dd) I F.le

The file of a laid file: what the kits walk.

Equations

• F.toIxFile = { cell := F.cell, strictMono := ⋯, cell_nonempty := ⋯ }

@[reducible]

noncomputable def DescriptiveComplexity.Draw.laidFile {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] (F : RegFile (Univ A R' P' dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) : LaidFile dt A R' P' (Univ A R' P' dt.KIx dt.dd)

The laid file a space-bounded program uses: one register per element of the universe, in the universe's own order, each naming its own tag's block and its own tuple.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixBack {L : FirstOrder.Language} (dt : Data L) {A R' P' I : Type} (lay : Layout dt A R' P' I) (zero one : A) (hdd : dt.dd0 ≤ dt.dd) (st : TapeSt dt A R' P' I) (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.SlotIx → A

The state, presented as a background, at an arbitrary index for the file: the value of each slot at each cell. The walked track of a pass is carved out of this by DescriptiveComplexity.Draw.Prog.trackTapeAt; everything else rides along.

What the file is indexed by is a parameter, because a clocked program cannot give every element of the universe a register and nothing here needs it to: a register's contents depend on its block, on the tuple it names, and on where it sits in the layout order, and on nothing else about the index. DescriptiveComplexity.Draw.Data.back is this at the diagonal, which is what a space-bounded program uses.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.reg = DescriptiveComplexity.Draw.bitVal zero one (∃ (u : I), r = lay.cell u)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.regFirst = DescriptiveComplexity.Draw.bitVal zero one (∃ (u : I), r = lay.cell u ∧ ∀ (y : I), lay.le u y)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.regLast = DescriptiveComplexity.Draw.bitVal zero one (∃ (u : I), r = lay.cell u ∧ ∀ (y : I), lay.le y u)
• dt.ixBack lay zero one hdd st r (DescriptiveComplexity.Draw.Slot.blk b) = DescriptiveComplexity.Draw.bitVal zero one (∃ (u : I), r = lay.cell u ∧ lay.blk u = b)
• dt.ixBack lay zero one hdd st r (DescriptiveComplexity.Draw.Slot.name j) = if h : ∃ (u : I), r = lay.cell u then lay.arg h.choose (Fin.castLE hdd j) else zero
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.mir = DescriptiveComplexity.Draw.bitVal zero one (DescriptiveComplexity.bitAtOf lay.cell st.mir r)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.tgt = DescriptiveComplexity.Draw.bitVal zero one (DescriptiveComplexity.bitAtOf lay.cell st.tgt r)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.sav = DescriptiveComplexity.Draw.bitVal zero one (DescriptiveComplexity.bitAtOf lay.cell st.sav r)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.val = DescriptiveComplexity.Draw.bitVal zero one (DescriptiveComplexity.bitAtOf lay.cell st.val r)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.wk = DescriptiveComplexity.Draw.bitVal zero one (st.wk r)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.bot = DescriptiveComplexity.Draw.bitVal zero one (st.bot r)
• dt.ixBack lay zero one hdd st r DescriptiveComplexity.Draw.Slot.ltp = DescriptiveComplexity.Draw.bitVal zero one (st.ltp r)
• dt.ixBack lay zero one hdd st r (DescriptiveComplexity.Draw.Slot.old i) = DescriptiveComplexity.Draw.bitVal zero one (st.old i r)
• dt.ixBack lay zero one hdd st r (DescriptiveComplexity.Draw.Slot.new i) = DescriptiveComplexity.Draw.bitVal zero one (st.new i r)

@[reducible]

noncomputable def DescriptiveComplexity.Draw.Data.diagLayout {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] (cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop) : Layout dt A R' P' (Univ A R' P' dt.KIx dt.dd)

The layout a space-bounded program's file has: one register per element of the universe, in the universe's own order, each naming its own tag's block and its own tuple.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.back {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] (cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop) (zero one : A) (hdd : dt.dd0 ≤ dt.dd) (st : TapeStD dt A R' P') (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.SlotIx → A

The state, presented as a background: DescriptiveComplexity.Draw.Data.ixBack at the layout a space-bounded program's file has.

Equations

• dt.back cell zero one hdd st r = dt.ixBack (dt.diagLayout cell) zero one hdd st r

The slot equations, at an arbitrary layout

Everything a slot of the background is depends on the layout and nothing else, so the equations that read one back are stated there once. The diagonal forms below are their instances at DescriptiveComplexity.Draw.Data.diagLayout, kept under their own names because that is what the whole evaluation layer rewrites with.

The slot equations, once

theorem DescriptiveComplexity.Draw.Data.back_of_not_reg {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {st : TapeStD dt A R' P'} {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ∀ (u : Univ A R' P' dt.KIx dt.dd), r ≠ cell u) (hwk : ¬st.wk r) (hbot : ¬st.bot r) (hltp : ¬st.ltp r) (hold : ∀ (i : dt.d.B.ι), ¬st.old i r) (hnew : ∀ (i : dt.d.B.ι), ¬st.new i r) : dt.back cell zero one hdd st r = fun (x : dt.SlotIx) => zero

Off the file, a state with no track set presents the blank. Every slot of the background at a cell that is nobody's register is either a permanent mark – existentially quantified over the registers, hence false there – or a register digit, false for the same reason, or one of the five per-cell tracks, which the hypotheses ask to be clear.

This is what makes the phase that builds a file a sweep of the file's stretch and nothing more: below the stretch and above it the background the phase has to produce is already the blank the machine started from, so the two ends of the sweep are the two ends of the file.

theorem DescriptiveComplexity.Draw.Data.back_old_congr {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {st : TapeStD dt A R' P'} (σ : dt.d.B.ι → (Univ A R' P' dt.KIx dt.dd → Prop) → Prop) {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ∀ (i : dt.d.B.ι), σ i r ↔ st.old i r) : dt.back cell zero one hdd { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } r = dt.back cell zero one hdd st r

The background reads the stage tracks at one cell. Two states differing in the old tracks alone present the same background at every cell where those tracks agree – the other slots being marks, register digits, or per-cell tracks the update leaves alone.

This is what a guessing phase needs: it rewrites the old tracks cell by cell, and the congruence is what says the cells it has not reached yet still read what they did.

What a state's scratch registers do not decide

The VAL loop threads SAV and TARGET and nothing else (DescriptiveComplexity.Draw.Data.roundEndSt_eq), so its rounds run at states that differ from the machinery's entry state in those two registers alone. ScratchEq names that relation, and the lemmas below say what it buys: every per-cell mark and track is shared, hence so is the background at every cell of the working area – the four register slots being DescriptiveComplexity.regBits, set at a register cell only.

def DescriptiveComplexity.Draw.Data.ScratchEq {L : FirstOrder.Language} (dt : Data L) {A R' P' I : Type} (st st' : TapeSt dt A R' P' I) : Prop

Two states differing in the two scratch registers alone: every mark and every track is shared, the saved mirror and the target need not be.

Equations

• dt.ScratchEq st st' = (st.wk = st'.wk ∧ st.mir = st'.mir ∧ st.val = st'.val ∧ st.old = st'.old ∧ st.new = st'.new ∧ st.bot = st'.bot ∧ st.ltp = st'.ltp)

theorem DescriptiveComplexity.Draw.Data.ScratchEq.symm {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {st st' : TapeSt dt A R' P' I} (h : dt.ScratchEq st st') : dt.ScratchEq st' st

ScratchEq is symmetric.

theorem DescriptiveComplexity.Draw.Data.ScratchEq.trans {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {st st' st'' : TapeSt dt A R' P' I} (h : dt.ScratchEq st st') (h' : dt.ScratchEq st' st'') : dt.ScratchEq st st''

ScratchEq is transitive.

theorem DescriptiveComplexity.Draw.Data.ScratchEq.tgt {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} {st st' : TapeStD dt A R' P'} (h : dt.ScratchEq st st') (Y : Univ A R' P' dt.KIx dt.dd → Prop) : dt.ScratchEq { mir := st.mir, tgt := Y, sav := st.sav, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } { mir := st'.mir, tgt := Y, sav := st'.sav, val := st'.val, old := st'.old, new := st'.new, wk := st'.wk, bot := st'.bot, ltp := st'.ltp }

ScratchEq survives writing the same target on both sides.

theorem DescriptiveComplexity.Draw.Data.ScratchEq.val {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} {st st' : TapeStD dt A R' P'} (h : dt.ScratchEq st st') (m : Univ A R' P' dt.KIx dt.dd → Prop) : dt.ScratchEq { mir := st.mir, tgt := st.tgt, sav := st.sav, val := m, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } { mir := st'.mir, tgt := st'.tgt, sav := st'.sav, val := m, old := st'.old, new := st'.new, wk := st'.wk, bot := st'.bot, ltp := st'.ltp }

ScratchEq survives writing the same VAL register on both sides.

theorem DescriptiveComplexity.Draw.Data.back_congr_off_reg {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {st st' : TapeStD dt A R' P'} (hwk : st.wk = st'.wk) (hbot : st.bot = st'.bot) (hltp : st.ltp = st'.ltp) (hold : st.old = st'.old) (hnew : st.new = st'.new) {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ¬∃ (u : Univ A R' P' dt.KIx dt.dd), r = cell u) : dt.back cell zero one hdd st r = dt.back cell zero one hdd st' r

Off the register file the background is blind to every register: the four register slots read DescriptiveComplexity.bitAtOf, which is set at a register cell only, so at a cell of the working area two states agree as soon as their per-cell marks and tracks do – whatever their mirror, their target, their saved mirror or their VAL content is. This is what lets the control of the VAL loop's threaded states be the control of the unthreaded ones: threading rewrites the two scratch registers, and the rounds read their background at the working cell.

theorem DescriptiveComplexity.Draw.Data.ScratchEq.ixBack {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {st st' : TapeSt dt A R' P' I} (h : dt.ScratchEq st st') {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ¬∃ (u : I), r = lay.cell u) : dt.ixBack lay zero one hdd st r = dt.ixBack lay zero one hdd st' r

The background at a working cell, off a ScratchEq, at an arbitrary layout: two states differing in the two scratch registers alone present the same background wherever no register is.

theorem DescriptiveComplexity.Draw.Data.ScratchEq.back {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {st st' : TapeStD dt A R' P'} (h : dt.ScratchEq st st') {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ¬∃ (u : Univ A R' P' dt.KIx dt.dd), r = cell u) : dt.back cell zero one hdd st r = dt.back cell zero one hdd st' r

The background at a working cell, off a ScratchEq.

The navigation by name, at an arbitrary layout

The three equations above are all a name scan reads, so the guard's reading is stated at the layout too. Only the uniqueness asks anything of the layout – DescriptiveComplexity.Draw.Layout.NameSep, that the marks tell the registers apart – and the elementwise layout has it because a register is its tag and its tuple.

The register a name identifies

Put the two halves together: on a layout whose marks tell its registers apart (DescriptiveComplexity.Draw.Layout.NameSep) and which has a register for every name (DescriptiveComplexity.Draw.Layout.HasName), the guard of a scan by name holds at one register of the file and nowhere else on it. That is exactly the pair of hypotheses DescriptiveComplexity.Draw.Prog.reaches_toCell asks for, so a caller's scan arrives at a register it can name.

This is what replaces the address-carrying random access at a clocked program's file: DescriptiveComplexity.Draw.SeekKit steps a marker until the walked mirror equals a target written across the file, which needs one register per address; a scan by name needs only the dd₀ coordinates the control already holds.

theorem DescriptiveComplexity.Draw.Data.nameGF_unique_addr {L : FirstOrder.Language} (dt : Data L) {A R' P' I : Type} {lay : Layout dt A R' P' I} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {stI : TapeSt dt A R' P' I} (hzo : zero ≠ one) (hinj : Function.Injective lay.cell) (hsep : lay.NameSep zero hdd) {Q : Type} {b : Fin dt.ko ⊕ Fin dt.ki} {cf : (Q → A) → Fin dt.dd0 → A} {fc : Q → A} {u : I} (hb : lay.blk u = some b) (ha : lay.arg u = padTup zero (cf fc)) {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : dt.nameGF one b cf fc (dt.ixBack lay zero one hdd stI r)) : r = lay.cell u

The name guard holds at exactly one address of the file: at the named register, and at no other register nor anywhere off the file. The stopping condition of a scan by name, in the shape a scan asks for.

The permanent marks at a register cell, and the navigation by name

The mark slots are stated existentially – “some element's cell, whose tag's block is b” – because the background is a function of the address. At a register cell the existential collapses, by injectivity of the cell family, and what is left is the mark of the element itself. Those three equations are what the navigation-by-name scans read: DescriptiveComplexity.Draw.Data.nameG holds at exactly one cell, the canonically padded cell of the element whose coordinates the control holds (DescriptiveComplexity.Draw.Data.nameG_unique), and nowhere off the register file.

theorem DescriptiveComplexity.Draw.Data.hasName_diagLayout {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} {zero : A} : (dt.diagLayout cell).HasName zero

The elementwise layout has a register for every name: a register is an element, and every block and tuple names one.

theorem DescriptiveComplexity.Draw.Data.nameG_cell {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {st : TapeStD dt A R' P'} (hzo : zero ≠ one) (hinj : Function.Injective cell) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (fc : Q → A) (u : Univ A R' P' dt.KIx dt.dd) : dt.nameG one b coord fc (dt.back cell zero one hdd st (cell u)) ↔ tagBlk u.1 = some b ∧ (∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → u.2 j = zero) ∧ ∀ (j : Fin dt.dd0), u.2 (Fin.castLE hdd j) = fc (coord j)

The coordinate-loop trips' guard, at a register cell.

theorem DescriptiveComplexity.Draw.Data.nameG_unique {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {cell : Univ A R' P' dt.KIx dt.dd → Univ A R' P' dt.KIx dt.dd → Prop} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {st : TapeStD dt A R' P'} (hzo : zero ≠ one) (hinj : Function.Injective cell) {Q : Type} {b : Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {fc : Q → A} {u u' : Univ A R' P' dt.KIx dt.dd} (h : dt.nameG one b coord fc (dt.back cell zero one hdd st (cell u))) (h' : dt.nameG one b coord fc (dt.back cell zero one hdd st (cell u'))) : u = u'

The coordinate-loop trips' guard identifies one cell.

The two ends of the file, at an arbitrary index

What a discharge asks of the regFirst and regLast slots is that they be set at one named cell and nowhere else, and that is a fact about the layout order alone: antisymmetry says the extreme index is unique, and the file is injective in nothing – the slot is read off the index, not off the address. So both are stated at the general index, and the elementwise forms are their diagonal.

theorem DescriptiveComplexity.Draw.Data.ixBack_regLast {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {I : Type} {lay : Layout dt A R' P' I} {st : TapeSt dt A R' P' I} (hlin : IsLinOrd lay.le) {gtop : I} (htop : ∀ (y : I), lay.le y gtop) (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.ixBack lay zero one hdd st r Slot.regLast = bitVal zero one (r = lay.cell gtop)

The file-top mark is the greatest index's cell.

theorem DescriptiveComplexity.Draw.Data.ixBack_regFirst {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {I : Type} {lay : Layout dt A R' P' I} {st : TapeSt dt A R' P' I} (hlin : IsLinOrd lay.le) {gbot : I} (hbot : ∀ (y : I), lay.le gbot y) (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.ixBack lay zero one hdd st r Slot.regFirst = bitVal zero one (r = lay.cell gbot)

The file-bottom mark is the least index's cell.