The tape the register channel hands over is the state the run reads

A program that lays its own file arrives at its evaluation with a background built by the sweep; a program that is handed its file has that background from time zero. This file says the two agree: the marks the register channel writes are, slot for slot, what DescriptiveComplexity.Draw.Data.ixBack reads off the entry state at the handed file.

Only two slots need an argument, and both are about the file's ends:

• regFirst – at this channel the first register is not the least element of the universe but the greatest carrying no argument block, which is why the mark is DescriptiveComplexity.Draw.regSlotMark and not DescriptiveComplexity.Draw.slotMark (isTopNonArg_iff_least_marked);
• regLast – the last register is the last element, the argument tags being the greatest (isGreatest_iff_greatest_marked).

Everything else is a tag decision the layout repeats (the block one-hots, the name slots, the padding flag) or a track that starts clear.

The two ends of the handed file

theorem DescriptiveComplexity.Draw.Data.exists_isTopNonArg {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Finite A] [Finite R'] [Finite P'] [Nonempty A] : ∃ (z : Univ A R' P' dt.KIx dt.dd), IsTopNonArg z

The element below the argument tags exists: the elements carrying no argument block are finitely many and not none, so one of them is greatest.

theorem DescriptiveComplexity.Draw.Data.arg_of_isGreatest {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Nonempty dt.KIx] {x : Univ A R' P' dt.KIx dt.dd} (hx : ∀ (y : Univ A R' P' dt.KIx dt.dd), tagTupleLe y x) : ∃ (i : dt.KIx), x.1 = Tag.arg i

The greatest element carries an argument block, provided there is one: the argument tags come last (DescriptiveComplexity.Draw.lt_arg).

theorem DescriptiveComplexity.Draw.Data.isTopNonArg_iff_least_marked {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] {Marked : Univ A R' P' dt.KIx dt.dd → Prop} (hmk : ∀ (x : Univ A R' P' dt.KIx dt.dd), Marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (hex : ∃ (z : Univ A R' P' dt.KIx dt.dd), IsTopNonArg z) {x : Univ A R' P' dt.KIx dt.dd} (hx : Marked x) : IsTopNonArg x ↔ ∀ (y : Univ A R' P' dt.KIx dt.dd), Marked y → tagTupleLe x y

The first register of the handed file is the element below the argument tags: the channel marks the argument elements and that one, and it is the least of them. This is the regFirst slot's whole content, and the reason the mark had to change.

theorem DescriptiveComplexity.Draw.Data.isGreatest_iff_greatest_marked {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] [Nonempty dt.KIx] {Marked : Univ A R' P' dt.KIx dt.dd → Prop} (hmk : ∀ (x : Univ A R' P' dt.KIx dt.dd), Marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) {x : Univ A R' P' dt.KIx dt.dd} : (∀ (y : Univ A R' P' dt.KIx dt.dd), tagTupleLe y x) ↔ ∀ (y : Univ A R' P' dt.KIx dt.dd), Marked y → tagTupleLe y x

The last register of the handed file is the last element: the argument tags being the greatest, the greatest element is one of the marked ones, so being greatest among them is being greatest. The regLast slot therefore needs no change.

The tape at time zero is the entry state's background

theorem DescriptiveComplexity.Draw.Data.startBack_initBackReg {L : FirstOrder.Language} {dt : Data L} {A R' PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite (NexPh (Option dt.KIx) PE)] [Finite dt.KIx] [Nonempty A] [Nonempty dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hR : PR.table.Reads) (hmark : ∀ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), PR.mark x = regSlotMark PR.zero PR.one ⋯ x) (hmk : ∀ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (hblank : ∀ (s : dt.SlotIx), PR.blank s = PR.zero) {v : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hv : ∀ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), PR.marked x → v ≠ wmRegSeg x) : startBack PR.initBackReg PR.one v = dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ (dt.nexEntrySt v)

The channel's tape, after the start step, is the entry state's background: what a program that lays its own file arrives at its evaluation with, a program handed its file has from the start. Slot for slot: the register flag and the block one-hots repeat the layout's, the name slots the element's own coordinates, the two end slots the file's ends (isTopNonArg_iff_least_marked, isGreatest_iff_greatest_marked), and every track is clear – except at the marker, where the start step sets wk and bot, and the entry state says the same.

theorem DescriptiveComplexity.Draw.Data.initBackReg_track_zero {L : FirstOrder.Language} {dt : Data L} {A R' PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite (NexPh (Option dt.KIx) PE)] [Finite dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hlin : IsLinOrd WMLe) (hR : PR.table.Reads) (hmark : ∀ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), PR.mark x = regSlotMark PR.zero PR.one ⋯ x) (hblank : ∀ (s : dt.SlotIx), PR.blank s = PR.zero) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) (s : dt.SlotIx) (hs : ¬Slot.IsFile s) : PR.initBackReg r s = PR.zero

Every track of the channel's tape is clear: a mark is a regSlotMark, whose tracks are all zero, and every other cell is blank. This is what the semantic half of a backward reading starts from – the tracks hold nothing until the machine writes them.

theorem DescriptiveComplexity.Draw.Data.tapeShape_initBackReg {L : FirstOrder.Language} {dt : Data L} {A R' PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite (NexPh (Option dt.KIx) PE)] [Finite dt.KIx] [Nonempty A] [Nonempty dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hR : PR.table.Reads) (hmark : ∀ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), PR.mark x = regSlotMark PR.zero PR.one ⋯ x) (hmk : ∀ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (hblank : ∀ (s : dt.SlotIx), PR.blank s = PR.zero) {v : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hv : ∀ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), PR.marked x → v ≠ wmRegSeg x) : TapeShape (regLaid hlin hord).toLayout PR.zero PR.one (dt.nexEntrySt v) PR.initBackReg

The tape the channel hands over is recognizable: the file's slots are the layout's (that is startBack_initBackReg, read at those slots alone, the start step touching only tracks), the four addressed tracks are clear, and every other track is a bit – the marks are regSlotMarks and the rest is blank. This is the base of an opening's reading.

What the marking gives the run

theorem DescriptiveComplexity.Draw.Data.hasInp_iff_regMarked {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (hmk : ∀ (x : Univ A R' P' dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (x : Univ A R' P' dt.KIx dt.dd) : WMHasInp x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x

The channel writes for an element exactly when the program marks it.

theorem DescriptiveComplexity.Draw.Data.hasInp_of_arg {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (hmk : ∀ (x : Univ A R' P' dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) {x : Univ A R' P' dt.KIx dt.dd} (hx : ∃ (k : dt.KIx), x.1 = Tag.arg k) : WMHasInp x

Every argument element carries input: the hargall the run asks for.

theorem DescriptiveComplexity.Draw.Data.hasInp_blkElt {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (hmk : ∀ (x : Univ A R' P' dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (zero : A) (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A) : WMHasInp (Tag.arg (toLex b), padTup zero c)

Every named register carries input: the harg the file's HasName asks for.

theorem DescriptiveComplexity.Draw.Data.hasInp_up {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (hmk : ∀ (x : Univ A R' P' dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (x y : Univ A R' P' dt.KIx dt.dd) (hxy : WMLe x y) (hx : WMHasInp x) : WMHasInp y

The elements the channel writes for are upward closed: above an argument element everything is an argument element, and above the one element below them everything is marked. This is the hup the file's bound (DescriptiveComplexity.wideRank_wmRegSeg_lt) asks for, and what puts the file under 2 ^ the number of marks.

theorem DescriptiveComplexity.Draw.Data.exists_regBotElt {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Nonempty A] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (hmk : ∀ (x : Univ A R' P' dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) : ∃ (z : Univ A R' P' dt.KIx dt.dd), WMHasInp z ∧ (∀ (y : Univ A R' P' dt.KIx dt.dd), WMHasInp y → WMLe z y) ∧ ∀ (i : dt.KIx), z.1 ≠ Tag.arg i

The element below the argument tags is marked and least among the marked ones: the bot the working area is measured against (DescriptiveComplexity.Draw.Data.work_regLaid).