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

theorem DescriptiveComplexity.Draw.Layout.blk_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) : lay.blk (lay.reg hhas b c) = some b

The named register is in the named block.

theorem DescriptiveComplexity.Draw.Layout.arg_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) : lay.arg (lay.reg hhas b c) = padTup zero c

The named register carries the named tuple, canonically padded.

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.

theorem DescriptiveComplexity.Draw.isLinOrd_laidFile_le {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} (hlin : IsLinOrd WMLe) : IsLinOrd (laidFile F hord).le

The elementwise file's layout order is linear, given that the universe's is and that the two agree – which is the hord every diagonal statement of the layer already carries.

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.diagLaid {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)] (RF : 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 elementwise file, laid out: one register per element of the universe, in the universe's own order, each naming its own tag's block and its own tuple. This is what a space-bounded program's register file is, read as a DescriptiveComplexity.Draw.LaidFile, so that the runs stated at an arbitrary file apply to it – its layout is DescriptiveComplexity.Draw.Data.diagLayout exactly, so its background is DescriptiveComplexity.Draw.Data.back.

Equations

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

theorem DescriptiveComplexity.Draw.Data.isLinOrd_diagLaid_le {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)] (RF : 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) (hlin : IsLinOrd WMLe) : IsLinOrd (dt.diagLaid RF hord).le

The elementwise layout order is linear, being the address order.

theorem DescriptiveComplexity.Draw.Data.wmLt_diagLaid_le {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)] (RF : 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) (u u' : Univ A R' P' dt.KIx dt.dd) : WMLt (dt.diagLaid RF hord).le u u' ↔ WMLt WMLe (id u) (id u')

The elementwise file names each element by itself, which is the identity embedding of DescriptiveComplexity.ixAddr.

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.

theorem DescriptiveComplexity.Draw.Data.ixBack_wk {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} (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.ixBack lay zero one hdd stI r Slot.wk = bitVal zero one (stI.wk r)

The marker slot, at an arbitrary layout.

theorem DescriptiveComplexity.Draw.Data.ixBack_of_not_reg {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} {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ∀ (u : I), r ≠ lay.cell u) (hwk : ¬stI.wk r) (hbot : ¬stI.bot r) (hltp : ¬stI.ltp r) (hold : ∀ (i : dt.d.B.ι), ¬stI.old i r) (hnew : ∀ (i : dt.d.B.ι), ¬stI.new i r) : dt.ixBack lay zero one hdd stI r = fun (x : dt.SlotIx) => zero

Off the file, a state with no track set presents the blank, at an arbitrary layout.

theorem DescriptiveComplexity.Draw.Data.ixBack_old_congr {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} (σ : 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 ↔ stI.old i r) : dt.ixBack lay zero one hdd { mir := stI.mir, tgt := stI.tgt, sav := stI.sav, val := stI.val, old := σ, new := stI.new, wk := stI.wk, bot := stI.bot, ltp := stI.ltp } r = dt.ixBack lay zero one hdd stI r

The background reads the stage tracks at one cell, at an arbitrary layout.

theorem DescriptiveComplexity.Draw.Data.ixBack_congr_off_reg {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 stI' : TapeSt dt A R' P' I} (hwk : stI.wk = stI'.wk) (hbot : stI.bot = stI'.bot) (hltp : stI.ltp = stI'.ltp) (hold : stI.old = stI'.old) (hnew : stI.new = stI'.new) {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ¬∃ (u : I), r = lay.cell u) : dt.ixBack lay zero one hdd stI r = dt.ixBack lay zero one hdd stI' r

Off the file the background is blind to every register, at an arbitrary layout.

theorem DescriptiveComplexity.Draw.Data.ixBack_blk_cell {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} (hinj : Function.Injective lay.cell) (u : I) (b : Option (Fin dt.ko ⊕ Fin dt.ki)) : dt.ixBack lay zero one hdd stI (lay.cell u) (Slot.blk b) = bitVal zero one (lay.blk u = b)

The block one-hot, at a register cell of an arbitrary layout.

theorem DescriptiveComplexity.Draw.Data.ixBack_pdd_cell {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} (hinj : Function.Injective lay.cell) (u : I) : dt.ixBack lay zero one hdd stI (lay.cell u) Slot.pdd = bitVal zero one (∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → lay.arg u j = zero)

The padding mark, at a register cell of an arbitrary layout.

theorem DescriptiveComplexity.Draw.Data.ixBack_name_cell {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} (hinj : Function.Injective lay.cell) (u : I) (j : Fin dt.dd0) : dt.ixBack lay zero one hdd stI (lay.cell u) (Slot.name j) = lay.arg u (Fin.castLE hdd j)

A name slot, at a register cell of an arbitrary layout.

The slot equations, once

theorem DescriptiveComplexity.Draw.Data.back_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) : dt.back cell zero one hdd st r Slot.reg = bitVal zero one (∃ (u : Univ A R' P' dt.KIx dt.dd), r = cell u)

The register mark: set exactly at the register cells – the equation every discharge's hrg is.

theorem DescriptiveComplexity.Draw.Data.back_wk {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.back cell zero one hdd st r Slot.wk = bitVal zero one (st.wk r)

The marker slot, read back.

theorem DescriptiveComplexity.Draw.Data.back_bot {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.back cell zero one hdd st r Slot.bot = bitVal zero one (st.bot r)

The bottom mark, read back.

theorem DescriptiveComplexity.Draw.Data.back_ltp {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.back cell zero one hdd st r Slot.ltp = bitVal zero one (st.ltp r)

The end mark, read back.

theorem DescriptiveComplexity.Draw.Data.back_name {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'} (j : Fin dt.dd0) (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.back cell zero one hdd st r (Slot.name j) = if h : ∃ (u : Univ A R' P' dt.KIx dt.dd), r = cell u then h.choose.2 (Fin.castLE hdd j) else zero

A name slot, read back: the coordinate the register's own index carries, and the designated zero where there is no register. Stated because the definition matches on the slot, so rw cannot reach the branch on its own.

theorem DescriptiveComplexity.Draw.Data.back_old {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'} (i : dt.d.B.ι) (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.back cell zero one hdd st r (Slot.old i) = bitVal zero one (st.old i r)

A stage track, read back.

theorem DescriptiveComplexity.Draw.Data.back_new {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'} (i : dt.d.B.ι) (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.back cell zero one hdd st r (Slot.new i) = bitVal zero one (st.new i r)

The next-stage track, read back.

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_scratch {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} (st : TapeStD dt A R' P') (X Y : Univ A R' P' dt.KIx dt.dd → Prop) : dt.ScratchEq { mir := st.mir, tgt := Y, sav := X, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } st

Rewriting the two scratch registers is a ScratchEq.

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.scratch {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} {st st' : TapeStD dt A R' P'} (h : dt.ScratchEq st st') (X Y : Univ A R' P' dt.KIx dt.dd → Prop) : dt.ScratchEq { mir := st.mir, tgt := Y, sav := X, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } { mir := st'.mir, tgt := Y, sav := X, val := st'.val, old := st'.old, new := st'.new, wk := st'.wk, bot := st'.bot, ltp := st'.ltp }

ScratchEq survives writing the same scratch registers on both sides.

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.ixScratch {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {st st' : TapeSt dt A R' P' I} (h : dt.ScratchEq st st') (X Y : I → Prop) : dt.ScratchEq { mir := st.mir, tgt := Y, sav := X, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } { mir := st'.mir, tgt := Y, sav := X, val := st'.val, old := st'.old, new := st'.new, wk := st'.wk, bot := st'.bot, ltp := st'.ltp }

ScratchEq survives writing the same save and target on both sides, at an arbitrary file.

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.

theorem DescriptiveComplexity.Draw.Data.ixNameGF_cell {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) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (cf : (Q → A) → Fin dt.dd0 → A) (fc : Q → A) (u : I) : dt.nameGF one b cf fc (dt.ixBack lay zero one hdd stI (lay.cell u)) ↔ lay.blk u = some b ∧ (∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → lay.arg u j = zero) ∧ ∀ (j : Fin dt.dd0), lay.arg u (Fin.castLE hdd j) = cf fc j

The name guard, at a register cell of an arbitrary layout: the register is in the named block, canonically padded, and carries the coordinates the control computes.

theorem DescriptiveComplexity.Draw.Data.ixNameGF_unique {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 u' : I} (h : dt.nameGF one b cf fc (dt.ixBack lay zero one hdd stI (lay.cell u))) (h' : dt.nameGF one b cf fc (dt.ixBack lay zero one hdd stI (lay.cell u'))) : u = u'

The name guard identifies one register, at a layout whose marks tell them apart.

theorem DescriptiveComplexity.Draw.Data.ixNot_nameGF_of_not_reg {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) {Q : Type} {b : Fin dt.ko ⊕ Fin dt.ki} {cf : (Q → A) → Fin dt.dd0 → A} {fc : Q → A} {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ∀ (u : I), r ≠ lay.cell u) : ¬dt.nameGF one b cf fc (dt.ixBack lay zero one hdd stI r)

Off the file the name guard fails, at an arbitrary layout: the block one-hot is clear there, so no scan stops in the working area.

theorem DescriptiveComplexity.Draw.Data.padTup_pad {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero : A) (c : Fin dt.dd0 → A) {j : Fin dt.dd} (hj : dt.dd0 ≤ ↑j) : padTup zero c j = zero

A named tuple is canonically padded.

theorem DescriptiveComplexity.Draw.Data.padTup_coord {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero : A) (c : Fin dt.dd0 → A) (hdd : dt.dd0 ≤ dt.dd) (j : Fin dt.dd0) : padTup zero c (Fin.castLE hdd j) = c j

A named tuple carries the control's coordinates.

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_named {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) {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)) : dt.nameGF one b cf fc (dt.ixBack lay zero one hdd stI (lay.cell u))

The name guard holds at the named register.

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.

theorem DescriptiveComplexity.Draw.Data.ixNameGF_iff {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) (hhas : lay.HasName zero) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (cf : (Q → A) → Fin dt.dd0 → A) (fc : Q → A) (u : I) : dt.nameGF one b cf fc (dt.ixBack lay zero one hdd stI (lay.cell u)) ↔ u = lay.reg hhas b (cf fc)

A computed name at a register says which register it is: on a layout that has a register for every name and tells them apart, the guard holds at exactly the register whose coordinates the control computes. The trips of the evaluation layer ask which cell they stopped at, and this is the answer, whatever function of the control the coordinates are.

theorem DescriptiveComplexity.Draw.Data.ixNameG_iff {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) (hhas : lay.HasName zero) {Q : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (fc : Q → A) (u : I) : dt.nameG one b coord fc (dt.ixBack lay zero one hdd stI (lay.cell u)) ↔ u = lay.reg hhas b fun (j : Fin dt.dd0) => fc (coord j)

The name guard at a register says which register it is, the coordinates read straight off the control: DescriptiveComplexity.Draw.Data.ixNameGF_iff at the coordinate slots the copy loops use.

theorem DescriptiveComplexity.Draw.Data.ixNot_nameG_of_not_reg {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) {Q : Type} {b : Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {fc : Q → A} {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ∀ (u : I), r ≠ lay.cell u) : ¬dt.nameG one b coord fc (dt.ixBack lay zero one hdd stI r)

Off the file the coordinate-loop trips' guard fails, at an arbitrary layout: the shape the evaluation layer's «the scan stopped nowhere else» arguments are written against.

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.back_blk_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'} (hinj : Function.Injective cell) (u : Univ A R' P' dt.KIx dt.dd) (b : Option (Fin dt.ko ⊕ Fin dt.ki)) : dt.back cell zero one hdd st (cell u) (Slot.blk b) = bitVal zero one (tagBlk u.1 = b)

The block one-hot, at a register cell.

theorem DescriptiveComplexity.Draw.Data.back_pdd_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'} (hinj : Function.Injective cell) (u : Univ A R' P' dt.KIx dt.dd) : dt.back cell zero one hdd st (cell u) Slot.pdd = bitVal zero one (∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → u.2 j = zero)

The padding mark, at a register cell.

theorem DescriptiveComplexity.Draw.Data.back_name_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'} (hinj : Function.Injective cell) (u : Univ A R' P' dt.KIx dt.dd) (j : Fin dt.dd0) : dt.back cell zero one hdd st (cell u) (Slot.name j) = u.2 (Fin.castLE hdd j)

A name slot, at a register cell: the element's own coordinate.

theorem DescriptiveComplexity.Draw.Data.nameGF_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) (cf : (Q → A) → Fin dt.dd0 → A) (fc : Q → A) (u : Univ A R' P' dt.KIx dt.dd) : dt.nameGF one b cf 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) = cf fc j

The name guard, at a register cell: the cell's element is in the named block, canonically padded, and carries the coordinates the control computes.

theorem DescriptiveComplexity.Draw.Data.nameSep_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} {hdd : dt.dd0 ≤ dt.dd} : (dt.diagLayout cell).NameSep zero hdd

The elementwise layout's marks tell its registers apart: a register is its tag and its tuple, so the block and the named coordinates spell it.

theorem DescriptiveComplexity.Draw.Data.padTup_eq_pad {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero : A) (c : Fin dt.dd0 → A) : padTup zero c = pad zero c

A named tuple is the padded one: DescriptiveComplexity.Draw.padTup and DescriptiveComplexity.Draw.pad are the same function, written once for the name a control holds and once for the geometry.

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.reg_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} (hdd : dt.dd0 ≤ dt.dd) (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A) : (dt.diagLayout cell).reg ⋯ b c = (Tag.arg (toLex b), padTup zero c)

At the elementwise layout the named register is the obvious one: the element whose tag is the block and whose tuple is the padded name. Chosen by DescriptiveComplexity.Draw.Layout.reg, pinned by NameSep.

theorem DescriptiveComplexity.Draw.Data.nameGF_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} {cf : (Q → A) → Fin dt.dd0 → A} {fc : Q → A} {u u' : Univ A R' P' dt.KIx dt.dd} (h : dt.nameGF one b cf fc (dt.back cell zero one hdd st (cell u))) (h' : dt.nameGF one b cf fc (dt.back cell zero one hdd st (cell u'))) : u = u'

The name guard identifies one cell: two register cells it holds at are the same. This is what a navigation-by-name scan needs of its stopping condition (DescriptiveComplexity.Draw.Prog.reaches_toCell).

theorem DescriptiveComplexity.Draw.Data.not_nameGF_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'} (hzo : zero ≠ one) {Q : Type} {b : Fin dt.ko ⊕ Fin dt.ki} {cf : (Q → A) → Fin dt.dd0 → A} {fc : Q → A} {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ∀ (u : Univ A R' P' dt.KIx dt.dd), r ≠ cell u) : ¬dt.nameGF one b cf fc (dt.back cell zero one hdd st r)

Off the register file the name guard fails: the block one-hot is clear there, so no scan stops in the working area.

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.

theorem DescriptiveComplexity.Draw.Data.not_nameG_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'} (hzo : zero ≠ one) {Q : Type} {b : Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {fc : Q → A} {r : Univ A R' P' dt.KIx dt.dd → Prop} (hr : ∀ (u : Univ A R' P' dt.KIx dt.dd), r ≠ cell u) : ¬dt.nameG one b coord fc (dt.back cell zero one hdd st r)

Off the register file the coordinate-loop trips' guard fails.

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.

theorem DescriptiveComplexity.Draw.Data.back_regLast {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)] {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'} (hlin : IsLinOrd WMLe) {gtop : Univ A R' P' dt.KIx dt.dd} (htop : ∀ (y : Univ A R' P' dt.KIx dt.dd), WMLe y gtop) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (r : Univ A R' P' dt.KIx dt.dd → Prop) : dt.back cell zero one hdd st r Slot.regLast = bitVal zero one (r = cell gtop)

The file-top mark is the greatest element's cell: given that the universe order is linear, the regLast slot is set exactly at the cell of the top element – the equation every discharge's hrl is.