A run, read as a table of tiles

The half of the drawing that turns an accepting run of a clocked wide machine into a tiling of the emitted square: the row of rank k is the configuration at time k, and a cell of that row is the tile the configuration puts there.

What a configuration puts in a cell

• the head's own cell carries head while the run still has a step to take, and halt once it has stopped – which is what lets a run shorter than the clock fill the rows above it, every one repeating the last configuration;
• the cell the head is about to enter carries the arrival, on the side the head comes from;
• every other cell carries sym, holding what the tape holds there.

The states, the symbols and the transitions of the machine are control elements of its universe – Sum.inr points – and a tile stores the element, so the reading DescriptiveComplexity.TilingHard.wpElt is used throughout, and loses nothing: a mark or an attribute of the instance holds of no address.

Control elements, read as elements

noncomputable def DescriptiveComplexity.TilingHard.wpElt {A : Type} [Nonempty A] (p : WPoint A) : A

The element a point of the machine's universe is, arbitrary at an address. Every point a mark or an attribute of the instance holds of is a control element, so nothing is lost where it is used.

Equations

• DescriptiveComplexity.TilingHard.wpElt (Sum.inl val) = Classical.arbitrary A
• DescriptiveComplexity.TilingHard.wpElt (Sum.inr x) = x

@[simp]

theorem DescriptiveComplexity.TilingHard.wpElt_inr {A : Type} [Nonempty A] (x : A) : wpElt (Sum.inr x) = x

A run, with its transitions named

A row for every step of the clock

The tile a configuration puts in a cell

noncomputable def DescriptiveComplexity.TilingHard.tileAt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] (g : ℕ → Config (WPoint A)) (tr : ℕ → WPoint A) (n k : ℕ) (cell : WPoint A) : TilePt A

The tile the run puts at a cell of a row: the head's cell carries the head while a step is left and the halt afterwards, the cell the head is entering carries the arrival on the side it comes from, and every other cell carries what the tape holds.

Equations

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

@[simp]

theorem DescriptiveComplexity.TilingHard.tileAt_head {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} (hh : (g k).head = cell) (hk : k < n) : tileAt g tr n k cell = (TileTag.head, ![wpElt ((g k).tape cell), wpElt (g k).state, wpElt (tr k)])

@[simp]

theorem DescriptiveComplexity.TilingHard.tileAt_halt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} (hh : (g k).head = cell) (hk : ¬k < n) : tileAt g tr n k cell = (TileTag.halt, ![wpElt ((g k).tape cell), wpElt (g k).state, wpElt ((g k).tape cell)])

@[simp]

theorem DescriptiveComplexity.TilingHard.tileAt_sym {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} (hh : (g k).head ≠ cell) (hnext : ¬(k < n ∧ (g (k + 1)).head = cell)) : tileAt g tr n k cell = (TileTag.sym, ![wpElt ((g k).tape cell), wpElt ((g k).tape cell), wpElt ((g k).tape cell)])