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

theorem DescriptiveComplexity.TilingHard.eq_inr_of_wpMark {A : Type} [Nonempty A] {R : A → Prop} {p : WPoint A} (h : wpMark R p) : p = Sum.inr (wpElt p)

A point carrying a mark of the instance is a control element.

theorem DescriptiveComplexity.TilingHard.wpMark_elt {A : Type} [Nonempty A] {R : A → Prop} {p : WPoint A} (h : wpMark R p) : R (wpElt p)

And the mark holds of the element it is.

theorem DescriptiveComplexity.TilingHard.wpAttr_elt {A : Type} [Nonempty A] {R : A → A → Prop} {p q : WPoint A} (h : wpAttr R p q) : R (wpElt p) (wpElt q)

And the attribute holds of the elements they are.

A run, with its transitions named

def DescriptiveComplexity.TilingHard.StepWith {V : Type} (M : TMData V) (c c' : Config V) (τ : V) : Prop

One step, with the transition it fires named: TMData.Step with its existential opened, so that a drawing may put the transition in a tile.

Equations

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

theorem DescriptiveComplexity.TilingHard.step_iff_stepWith {V : Type} {M : TMData V} {c c' : Config V} : M.Step c c' ↔ ∃ (τ : V), StepWith M c c' τ

theorem DescriptiveComplexity.TilingHard.exists_runData {V : Type} {M : TMData V} [Nonempty V] (h : M.Accepts) : ∃ (g : ℕ → Config V) (tr : ℕ → V) (n : ℕ), M.IsInit (g 0) ∧ n < Nat.card { p : V // M.Posn p } ∧ (∀ (i : ℕ), n ≤ i → g i = g n) ∧ M.Acc (g n).state ∧ ∀ i < n, StepWith M (g i) (g (i + 1)) (tr i)

An accepting run, as a sequence with its transitions: the configurations at every time, the transition fired at every step before the last, and the run standing still afterwards.

theorem DescriptiveComplexity.TilingHard.exists_runDataSpace {V : Type} {M : TMData V} [Nonempty V] (h : M.AcceptsSpace) : ∃ (g : ℕ → Config V) (tr : ℕ → V) (n : ℕ), M.IsInit (g 0) ∧ (∀ (i : ℕ), n ≤ i → g i = g n) ∧ M.Acc (g n).state ∧ ∀ i < n, StepWith M (g i) (g (i + 1)) (tr i)

An accepting run in bounded space, as a sequence with its transitions: the same reading as DescriptiveComplexity.TilingHard.exists_runData for a machine with no clock – the run is still finite, only its length is not bounded by the instance.

theorem DescriptiveComplexity.TilingHard.head_posn {V : Type} {M : TMData V} {g : ℕ → Config V} {tr : ℕ → V} {n : ℕ} (hinit : M.IsInit (g 0)) (hfreeze : ∀ (i : ℕ), n ≤ i → g i = g n) (hstep : ∀ i < n, StepWith M (g i) (g (i + 1)) (tr i)) (k : ℕ) : M.Posn (g k).head

The head stands on a position at every time: it starts on the least one and a step moves it to a neighbor.

A row for every step of the clock

theorem DescriptiveComplexity.TilingHard.exists_wideRank_eq {A : Type} [Finite A] [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) {k : ℕ} (hk : k < Nat.card { p : WPoint A // (wideData A).Posn p }) : ∃ (s : A → Prop), wideRank s = k

Every rank below the number of addresses is taken: the rank map is injective into as many numbers as there are addresses, so it is onto them. That is what gives the drawing a row for every step of the clock, the clock counting the addresses.

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)])

theorem DescriptiveComplexity.TilingHard.tileAt_arr {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) (hnext : (g (k + 1)).head = cell) : tileAt g tr n k cell = (if WMRight (wpElt (tr k)) then TileTag.arrL else TileTag.arrR, ![wpElt ((g k).tape cell), wpElt (g (k + 1)).state, wpElt ((g k).tape cell)])

theorem DescriptiveComplexity.TilingHard.tpSym_tileAt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} : tpSym (tileAt g tr n k cell) = wpElt ((g k).tape cell)

The symbol a tile of the table holds is what the tape holds there.