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)

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

What stands above a cell

The head of a row comes from the row below

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

The run reaches the accepting row

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

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

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.