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

Every cell carries a tile

Some cell carries an accepting tile

One row becomes the next

Neighbors in one row

The bottom row is the initial tape

The two edge columns

The table is a tiling

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.