A tiling of the emitted square is an accepting run

The backward half of the hardness. A tiling is read row by row: the row of rank k is the configuration at time k, and the whole argument is that each row holds at most one head, and the row above it is the step that head takes.

Why a row holds at most one head

A head in a row is either a head that halted below it, or one a neighbor sent: the vertical rule lets nothing else stand above a symbol. A neighbor that sends one is a head moving that way, by the horizontal rule, so the head of a row is determined by the head of the row below it and the transition that head fires – which is why a tile carries the transition and an arrival is a tile of its own.

The two edge columns are where this argument would otherwise fail, and why DescriptiveComplexity.TileData.EdgeL and EdgeR are part of a tiling: an arrival at the leftmost column is sent by nothing, so without a border condition a head would appear there out of nowhere, carrying whatever state it liked.

What is read off a row

The drawing is packaged as DescriptiveComplexity.TilingHard.TileRun – rows numbered by the clock, columns the machine's addresses – so the coordinates of the emitted square are translated once and the argument itself is a plain induction on the row number.

def DescriptiveComplexity.TilingHard.IsHeadTile {A : Type} (p : TilePt A) : Prop

A cell holding a head, halted or not: the two tags an accepting tile may carry, and the two a tiling never puts side by side.

Equations

• DescriptiveComplexity.TilingHard.IsHeadTile p = (p.1 = DescriptiveComplexity.TileTag.head ∨ p.1 = DescriptiveComplexity.TileTag.halt)

def DescriptiveComplexity.TilingHard.wideDataOf (A : Type) [FirstOrder.Language.wide.Structure A] (Inp : WPoint A → WPoint A → Prop) : TMData (WPoint A)

The wide machine an instance describes, at a given input description: the machine of DescriptiveComplexity.wideData with its tape described by the given relation, which is the one thing the clocked machine and the space-bounded one disagree on.

Equations

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

structure DescriptiveComplexity.TilingHard.TileRun (A : Type) [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (Inp : WPoint A → WPoint A → Prop) : Type

A drawing of a run, read at the machine's own coordinates: the rows numbered by time, the columns the addresses of the machine, and every condition a tiling puts on them. The bottom row is stated as the machine's initial tape, so the same drawing serves whichever way that tape is described.

• rows : ℕ

  The number of rows.

• tl : ℕ → (A → Prop) → TilePt A

  The tile in a column of a row.

• tile (k : ℕ) (s : A → Prop) : TPTile (self.tl k s)

  Every cell carries a tile.

• start : TPStart (self.tl 0 fun (x : A) => False)

  The corner carries the machine's start.

• first (s : A → Prop) : (s ≠ fun (x : A) => False) → TPNoHead (self.tl 0 s) ∧ (Inp (Sum.inl s) (Sum.inr (tpSym (self.tl 0 s))) ∨ (∀ (b : WPoint A), ¬Inp (Sum.inl s) b) ∧ WMBlank (tpSym (self.tl 0 s)))

  Every other column of the bottom row holds no head, and holds what the machine's initial tape holds there.

• edgeL (k : ℕ) : TPEdgeL (self.tl k fun (x : A) => False)

  The leftmost column carries no arrival from the left.

• edgeR (k : ℕ) : TPEdgeR (self.tl k fun (x : A) => True)

  Nor the rightmost one an arrival from the right.

• horiz (k : ℕ) (s t : A → Prop) : WMIncr WMLe s t → TPHoriz (self.tl k s) (self.tl k t)

  Neighbors in a row agree.

• vert (k : ℕ) (s : A → Prop) : k + 1 < self.rows → TPVert (self.tl k s) (self.tl (k + 1) s)

  And one row becomes the next.

• accRow : ℕ

  The row of the accepting cell.

• accCol : A → Prop

  And its column.

• accRow_lt : self.accRow < self.rows

  The accepting cell is inside the square.

• acc : TPAcc (self.tl self.accRow self.accCol)

  And it carries an accepting tile.

Neighboring columns

theorem DescriptiveComplexity.TilingHard.exists_wmIncr_of_ne_top {A : Type} [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {s : A → Prop} (hs : s ≠ fun (x : A) => True) : ∃ (t : A → Prop), WMIncr WMLe s t

Every column but the last has one to its right.

theorem DescriptiveComplexity.TilingHard.exists_wmIncr_of_ne_bot {A : Type} [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {t : A → Prop} (ht : t ≠ fun (x : A) => False) : ∃ (s : A → Prop), WMIncr WMLe s t

And every column but the first one to its left, which is what justifies an arrival that is not at the edge.

theorem DescriptiveComplexity.TilingHard.wmIncr_left_unique {A : Type} [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {s s' t : A → Prop} (h : WMIncr WMLe s t) (h' : WMIncr WMLe s' t) : s = s'

A column has one column to its left at most.

What stands above a cell

theorem DescriptiveComplexity.TilingHard.isHeadTile_or_noHead {A : Type} [FirstOrder.Language.wide.Structure A] {p : TilePt A} (h : TPTile p) : IsHeadTile p ∨ TPNoHead p

A cell holds a head or holds none.

theorem DescriptiveComplexity.TilingHard.not_isHeadTile_of_noHead {A : Type} {p : TilePt A} (h : TPNoHead p) : ¬IsHeadTile p

And not both.

theorem DescriptiveComplexity.TilingHard.tpSym_vert {A : Type} [FirstOrder.Language.wide.Structure A] {p q : TilePt A} (h : TPVert p q) (hp : TPNoHead p ∨ p.1 = TileTag.halt) : tpSym q = tpSym p

A cell that holds no head keeps its symbol, whatever stands above it.

theorem DescriptiveComplexity.TilingHard.tag_of_head_above {A : Type} [FirstOrder.Language.wide.Structure A] {p q : TilePt A} (hp : TPTile p) (h : TPVert p q) (hq : IsHeadTile q) : p.1 = TileTag.halt ∨ p.1 = TileTag.arrL ∨ p.1 = TileTag.arrR

Nothing but a head or an arrival puts a head above it: above a symbol stands a cell with no head, and above a head the cell the head has left.

The head of a row comes from the row below

theorem DescriptiveComplexity.TilingHard.head_from {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) {k : ℕ} {s : A → Prop} (hk : k + 1 < R.rows) (h : IsHeadTile (R.tl (k + 1) s)) : (R.tl k s).1 = TileTag.halt ∧ tpState (R.tl (k + 1) s) = tpState (R.tl k s) ∨ ∃ (e : A → Prop), (R.tl k e).1 = TileTag.head ∧ (WMRight (tpTr (R.tl k e)) ∧ WMIncr WMLe e s ∨ ¬WMRight (tpTr (R.tl k e)) ∧ WMIncr WMLe s e) ∧ WMDst (tpTr (R.tl k e)) (tpState (R.tl (k + 1) s))

Where a head comes from: either it stood in the same column and halted, or the head of a neighboring column moved into it – and then that head's transition names the state it arrives in and the direction it came from.

theorem DescriptiveComplexity.TilingHard.head_zero {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) : IsHeadTile (R.tl 0 fun (x : A) => False)

The bottom row holds one head, at the corner: the corner carries the machine's start, and every other column the initial tape, which holds none.

theorem DescriptiveComplexity.TilingHard.eq_bot_of_head_zero {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) {s : A → Prop} (h : IsHeadTile (R.tl 0 s)) : s = fun (x : A) => False

And it is the only one.

theorem DescriptiveComplexity.TilingHard.head_unique {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) {k : ℕ} : k < R.rows → ∀ {s t : A → Prop}, IsHeadTile (R.tl k s) → IsHeadTile (R.tl k t) → s = t

A row holds one head at most. A head is either one that halted below it or one a neighbor sent, and the neighbor that sends one is the head of the row below moving that way; so the head of a row is determined by the head of the row below and the transition it fires.

theorem DescriptiveComplexity.TilingHard.exists_head_below {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) {k : ℕ} (hk : k + 1 < R.rows) (h : ∃ (s : A → Prop), IsHeadTile (R.tl (k + 1) s)) : ∃ (e : A → Prop), IsHeadTile (R.tl k e)

A row with a head stands on one below it: nothing sends a head into a row whose own row below has none.

The run a tiling draws

noncomputable def DescriptiveComplexity.TilingHard.headCol {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (k : ℕ) : A → Prop

The column the head of a row stands in, arbitrary in a row with no head.

Equations

• DescriptiveComplexity.TilingHard.headCol R k = if h : ∃ (s : A → Prop), DescriptiveComplexity.TilingHard.IsHeadTile (R.tl k s) then h.choose else fun (x : A) => False

theorem DescriptiveComplexity.TilingHard.rows_pos {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) : 0 < R.rows

A square has a row: the accepting cell stands in one.

theorem DescriptiveComplexity.TilingHard.headCol_spec {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) {k : ℕ} (h : ∃ (s : A → Prop), IsHeadTile (R.tl k s)) : IsHeadTile (R.tl k (headCol R k))

theorem DescriptiveComplexity.TilingHard.headCol_eq {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) {k : ℕ} (hk : k < R.rows) {s : A → Prop} (hs : IsHeadTile (R.tl k s)) : headCol R k = s

And it is the column of the head.

theorem DescriptiveComplexity.TilingHard.noHead_of_ne {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) {k : ℕ} (hk : k < R.rows) {d : A → Prop} (hd : d ≠ headCol R k) : TPNoHead (R.tl k d)

Every other column of a row holds no head, the head being unique.

noncomputable def DescriptiveComplexity.TilingHard.cfgAt {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (b₀ : A) (k : ℕ) : Config (WPoint A)

The configuration a row is: the head in its column, the state that head carries, and the symbols of the row on the tape. The control points hold a blank, which is what the machine's initial tape asks of them.

Equations

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

theorem DescriptiveComplexity.TilingHard.isInit_cfgAt {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) (b₀ : A) (hb : WMBlank b₀) (hctrl : ∀ (x : A) (b : WPoint A), ¬Inp (Sum.inr x) b) (hbot : ∀ (b : WPoint A), ¬Inp (Sum.inl fun (x : A) => False) b) : (wideDataOf A Inp).IsInit (cfgAt R b₀ 0)

The bottom row is an initial configuration: the head at the corner in a start state, the cell of an element carrying its input symbol and every other cell a blank.

theorem DescriptiveComplexity.TilingHard.step_or_eq {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) (b₀ : A) {k : ℕ} (hk : k + 1 < R.rows) (hup : ∃ (s : A → Prop), IsHeadTile (R.tl (k + 1) s)) : (wideDataOf A Inp).Step (cfgAt R b₀ k) (cfgAt R b₀ (k + 1)) ∨ cfgAt R b₀ (k + 1) = cfgAt R b₀ k

The row above is the step the head takes, or the same configuration again where the head has halted.

The run reaches the accepting row

theorem DescriptiveComplexity.TilingHard.stepsIn_cfgAt {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hlin : IsLinOrd WMLe) (b₀ : A) {k : ℕ} : k < R.rows → (∃ (s : A → Prop), IsHeadTile (R.tl k s)) → ∃ j ≤ k, (wideDataOf A Inp).StepsIn j (cfgAt R b₀ 0) (cfgAt R b₀ k)

A row with a head stands a bounded number of steps above the bottom row: each row below it is either the step its head takes or the same configuration again, where that head has halted.

theorem DescriptiveComplexity.TilingHard.accepts_of_tileRun {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hwf : WideWF A) (hctrl : ∀ (x : A) (b : WPoint A), ¬Inp (Sum.inr x) b) (hbot : ∀ (b : WPoint A), ¬Inp (Sum.inl fun (x : A) => False) b) (hrows : R.rows ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) : (wideDataOf A Inp).Accepts

A drawing is an accepting run of the machine: the accepting cell holds a head, so the row it stands in is a configuration the run reaches, in fewer steps than there are addresses.

theorem DescriptiveComplexity.TilingHard.acceptsSpace_of_tileRun {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {Inp : WPoint A → WPoint A → Prop} (R : TileRun A Inp) (hwf : WideWF A) (hctrl : ∀ (x : A) (b : WPoint A), ¬Inp (Sum.inr x) b) (hbot : ∀ (b : WPoint A), ¬Inp (Sum.inl fun (x : A) => False) b) : (wideDataOf A Inp).AcceptsSpace

And an accepting run in bounded space, where the drawing has no clock to answer to: the same run, with its length forgotten.

A tiling of the emitted square, read at the machine's coordinates

theorem DescriptiveComplexity.TilingHard.isLinOrd_of_tileWF {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (h : IsLinOrd (wideTileData (TilePt A)).Le) : IsLinOrd WMLe

The order a tiling promises is the machine's own, read at the digits: they are one per element, and the emitted order between two of them is the instance's.

noncomputable def DescriptiveComplexity.TilingHard.rowAt {A : Type} [FirstOrder.Language.wide.Structure A] (k : ℕ) : A → Prop

The address of a given rank, which is how the rows of the square are numbered by the clock.

Equations

• DescriptiveComplexity.TilingHard.rowAt k = if h : ∃ (s : A → Prop), DescriptiveComplexity.wideRank s = k then h.choose else fun (x : A) => False

theorem DescriptiveComplexity.TilingHard.wideRank_rowAt {A : Type} [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {k : ℕ} (hk : k < Nat.card { p : WPoint A // (wideData A).Posn p }) : wideRank (rowAt k) = k

theorem DescriptiveComplexity.TilingHard.rowAt_zero {A : Type} [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) : rowAt 0 = fun (x : A) => False

The bottom row is the empty address, where the machine's head starts.

theorem DescriptiveComplexity.TilingHard.wmIncr_rowAt {A : Type} [Finite A] [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {k : ℕ} (hk : k + 1 < Nat.card { p : WPoint A // (wideData A).Posn p }) : WMIncr WMLe (rowAt k) (rowAt (k + 1))

And one row above another is the increment of its address.

The backward half

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

A tiling of the emitted square is an accepting run of the machine. The square's coordinates are the machine's addresses, so a row is a configuration and the row above it the step its head takes; the promises the machine owes are carried by the start tile at the corner.