An accepting run tiles the emitted square

The forward half of the hardness: the table of DescriptiveComplexity.TilingHard.tileAt is a tiling of the square the reduction emits. Each of the five conditions is one fact about the run –

• every cell carries a tile, because a head tile carries the transition the step fires and the machine's own promises say it applies;
• some cell carries an accepting tile, at the row of the accepting configuration;
• the bottom row is the initial tape, with the head at the corner;
• horizontal neighbors agree, because the head is unique and an arrival stands next to it;
• vertical neighbors agree, because a step writes under the head and leaves every other cell alone.

def DescriptiveComplexity.TilingHard.addrOf {A : Type} : WPoint (TilePt A) → A → Prop

The address a coordinate of the emitted grid is.

Equations

• DescriptiveComplexity.TilingHard.addrOf (Sum.inl u) = fun (a : A) => u (DescriptiveComplexity.tpDig a)
• DescriptiveComplexity.TilingHard.addrOf (Sum.inr val) = fun (x : A) => False

@[simp]

theorem DescriptiveComplexity.TilingHard.addrOf_tpCol {A : Type} (s : A → Prop) : addrOf (Sum.inl (tpCol s)) = s

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

The table a run draws: the row of rank k is the configuration at time k, and its cell at a column is the tile that configuration puts there.

Equations

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

Every cell carries a tile

theorem DescriptiveComplexity.TilingHard.tpTile_tileAt {A : Type} [Nonempty A] [LinearOrder A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) (k : ℕ) (cell : WPoint A) : TPTile (tileAt g tr n k cell)

A head tile carries a transition the machine may fire, which is all DescriptiveComplexity.TPTile asks of it; every other kind of tile asks nothing.

Some cell carries an accepting tile

theorem DescriptiveComplexity.TilingHard.tpAcc_tileAt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hacc : (wideRegData A).Acc (g n).state) : TPAcc (tileAt g tr n n (g n).head)

The accepting configuration's head cell carries an accepting tile: the run has stopped there, so the tile is the halt, and it carries the accepting state.

One row becomes the next

theorem DescriptiveComplexity.TilingHard.tpNoHead_tileAt {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) : TPNoHead (tileAt g tr n k cell)

A cell the head is not on carries no head.

theorem DescriptiveComplexity.TilingHard.eq_of_not_lt {A : Type} {g : ℕ → Config (WPoint A)} {n k : ℕ} (hfreeze : ∀ (i : ℕ), n ≤ i → g i = g n) (hk : ¬k < n) : g (k + 1) = g k

After the last step the run stands still.

theorem DescriptiveComplexity.TilingHard.head_ne_next {A : Type} [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) (hk : k < n) : (g k).head ≠ (g (k + 1)).head

A step moves the head, so the cell it leaves is not the cell it enters.

theorem DescriptiveComplexity.TilingHard.tape_frame {A : Type} [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) (hfreeze : ∀ (i : ℕ), n ≤ i → g i = g n) (hh : (g k).head ≠ cell) : (g (k + 1)).tape cell = (g k).tape cell

A step writes under the head and leaves every other cell alone.

theorem DescriptiveComplexity.TilingHard.tpVert_tileAt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) (hfreeze : ∀ (i : ℕ), n ≤ i → g i = g n) (k : ℕ) (cell : WPoint A) : TPVert (tileAt g tr n k cell) (tileAt g tr n (k + 1) cell)

The row above is the step's: the head's cell holds what the step wrote, the cell the head is entering becomes the head, and every other cell copies itself.

Neighbors in one row

theorem DescriptiveComplexity.TilingHard.head_eq_of_tileAt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} (h : (tileAt g tr n k cell).1 = TileTag.head ∨ (tileAt g tr n k cell).1 = TileTag.halt) : (g k).head = cell

A head or a halt tile stands where the head stands.

theorem DescriptiveComplexity.TilingHard.head_of_tileAt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} (h : (tileAt g tr n k cell).1 = TileTag.head) : (g k).head = cell ∧ k < n

A head tile is the head, with a step left to take.

theorem DescriptiveComplexity.TilingHard.arr_of_tileAt {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n k : ℕ} {cell : WPoint A} {right : Bool} (h : (tileAt g tr n k cell).1 = if right = true then TileTag.arrL else TileTag.arrR) : (g k).head ≠ cell ∧ k < n ∧ (g (k + 1)).head = cell ∧ (WMRight (wpElt (tr k)) ↔ right = true)

An arrival is the cell the head is entering, from the left when the transition moves right.

theorem DescriptiveComplexity.TilingHard.tpTr_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) : tpTr (tileAt g tr n k cell) = wpElt (tr k)

The transition a head tile of the table carries is the one the step fires.

theorem DescriptiveComplexity.TilingHard.tpState_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) : tpState (tileAt g tr n k cell) = wpElt (g (k + 1)).state

The state an arrival of the table carries is the state the step reaches.

theorem DescriptiveComplexity.TilingHard.tileAt_arr_tag {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).1 = if WMRight (wpElt (tr k)) then TileTag.arrL else TileTag.arrR

The tag an arrival of the table carries names the side the head comes from.

theorem DescriptiveComplexity.TilingHard.wmRight_iff_right {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {p : WPoint A} (htr : (wideRegData A).Tr p) : (wideRegData A).Right p ↔ WMRight (wpElt p)

A transition moving right, read at the element it is.

theorem DescriptiveComplexity.TilingHard.tpHoriz_tileAt {A : Type} [Nonempty A] [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hlin : IsLinOrd WMLe) (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) {cL cR : WPoint A} (hs : SuccPos (wideRegData A).Le (wideRegData A).Posn cL cR) (k : ℕ) : TPHoriz (tileAt g tr n k cL) (tileAt g tr n k cR)

Neighboring cells of a row agree: the head is unique, so no two heads stand side by side; and the arrival next to it is on the side the transition moves, since the head moves to the neighbor in that direction.

The bottom row is the initial tape

theorem DescriptiveComplexity.TilingHard.wtHasFirst_tileStr {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (p : TilePt A) : WTHasFirst p ↔ TPDig p ∧ WMHasInp (p.2 0)

The elements the bottom row is described at are the ones carrying input: a digit whose element has an input symbol, since a cell holding that symbol and no head is always a tile of the emitted instance.

theorem DescriptiveComplexity.TilingHard.wmFileSeg_tpCol {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (s : A → Prop) (x : A) : WMFileSeg WTLe WTHasFirst (tpCol s) (tpDig x) ↔ WMRegSeg s x

The cells of the emitted file are the machine's register cells: a coordinate is a cell of the digit of x exactly when the address it is is the machine's cell of x.

theorem DescriptiveComplexity.TilingHard.wtpFirst_tpCol {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (s : A → Prop) (t : TilePt A) : (wideTileData (TilePt A)).First (Sum.inl (tpCol s)) (Sum.inr t) ↔ ∃ (x : A) (a : A), WMRegSeg s x ∧ WMInp x a ∧ TPNoHead t ∧ tpSym t = a

The bottom row of the emitted tiling is the machine's initial tape: the cell of an element may carry a tile holding that element's input symbol, and no head.

theorem DescriptiveComplexity.TilingHard.not_wmRegSeg_bot {A : Type} [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {x a : A} (hinp : WMInp x a) : ¬WMRegSeg (fun (x : A) => False) x

The empty address is no register cell, so the machine starts on a blank.

theorem DescriptiveComplexity.TilingHard.first_tableTiling {A : Type} [Nonempty A] [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hwf : WideWF A) (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) (hinit : (wideRegData A).IsInit (g 0)) {x y : WPoint (TilePt A)} (hx : (wideTileData (TilePt A)).Posn x) (hy : MinPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn y) : (MinPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn x → (wideTileData (TilePt A)).Start (tableTiling g tr n x y)) ∧ (¬MinPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn x → (wideTileData (TilePt A)).FirstTile x (tableTiling g tr n x y))

The bottom row the table draws is one the description allows: the corner carries the machine's start – the head, on the blank cell it begins on – and every other column carries the input symbol of its element, or the blank where the description names none.

The two edge columns

theorem DescriptiveComplexity.TilingHard.tpEdgeL_tileAt {A : Type} [Nonempty A] [Finite A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hlin : IsLinOrd WMLe) (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) {cell : WPoint A} (hmin : MinPos (wideRegData A).Le (wideRegData A).Posn cell) (k : ℕ) : TPEdgeL (tileAt g tr n k cell)

The head never arrives from the left at the first cell: an arrival from the left is a step moving right into that cell, and nothing lies below the least position.

theorem DescriptiveComplexity.TilingHard.tpEdgeR_tileAt {A : Type} [Nonempty A] [Finite A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hlin : IsLinOrd WMLe) (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) {cell : WPoint A} (hmax : MaxPos (wideRegData A).Le (wideRegData A).Posn cell) (k : ℕ) : TPEdgeR (tileAt g tr n k cell)

And never from the right at the last cell: an arrival from the right is a step moving left into that cell, and nothing lies above the greatest position.

The table is a tiling

theorem DescriptiveComplexity.TilingHard.tableTiling_tpCol {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (s r : A → Prop) : tableTiling g tr n (Sum.inl (tpCol s)) (Sum.inl (tpCol r)) = Sum.inr (tileAt g tr n (wideRank r) (Sum.inl s))

The tile the table puts at a coordinate of the emitted square, read at the machine's own address and time.

theorem DescriptiveComplexity.TilingHard.isTiling_tableTiling {A : Type} [Nonempty A] [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hwf : WideWF A) (hinit : (wideRegData A).IsInit (g 0)) (hlt : n < Nat.card { p : WPoint A // (wideRegData A).Posn p }) (hfreeze : ∀ (i : ℕ), n ≤ i → g i = g n) (hacc : (wideRegData A).Acc (g n).state) (hstep : ∀ i < n, StepWith (wideRegData A) (g i) (g (i + 1)) (tr i)) : (wideTileData (TilePt A)).IsTiling (tableTiling g tr n)

An accepting run draws a tiling of the emitted square. Each of the five conditions is one fact about the run: every cell carries a tile because a head tile carries the transition the step fires; the bottom row is the initial tape; neighbors in a row agree because the head is unique; one row becomes the next because a step writes under the head and leaves every other cell alone; and the accepting configuration's own cell carries an accepting tile.

theorem DescriptiveComplexity.TilingHard.tileable_of_accepts {A : Type} [Nonempty A] [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hwf : WideWF A) (h : (wideRegData A).Accepts) : (wideTileData (TilePt A)).WellFormed ∧ (wideTileData (TilePt A)).Tileable

An accepting run makes the emitted square tileable, which is the forward half of the hardness: the table the run draws is a tiling.